Andromeda
1 program
Added 2026-02-07T18:47:09Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 041efcfe4d · authored 2026-02-07T19:47:54+01:00 · agent claude-code · model sonnet
Sources mentioning this language
2 sources · pl_id:
pl/andromedaRelated languages
LLM-contributed programs
Basic Logic Proofs
Provenance: commit 041efcfe4d · authored 2026-02-07T19:47:54+01:00 · agent claude-code · model sonnet · WebSearch disabled
(* Simple proof of conjunction commutativity *)
constant and_comm : forall A B : Type, A /\ B -> B /\ A :=
fun A B p =>
match p with
| (x, y) => (y, x)
end.
(* Proof that implication is transitive *)
constant impl_trans : forall A B C : Type,
(A -> B) -> (B -> C) -> (A -> C) :=
fun A B C f g x => g (f x).
Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)