Milawa
1 program
Added 2026-03-13T10:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit b90822d758 · authored 2026-03-13T04:24:51+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
List Append with Proof
Provenance: commit b90822d758 · authored 2026-03-13T04:24:51+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
;;; Milawa: append function definition and proof
;;; From the Milawa theorem prover (Jared Davis, UT Austin)
(%defun app (x y)
(if (consp x)
(cons (car x) (app (cdr x) y))
y))
(%prove (%theorem app-of-nil
(equal (app nil y) y)))
(%auto)
(%qed)
(%prove (%theorem consp-of-app
(equal (consp (app x y))
(if (consp x)
t
(consp y)))))
(%induct (len x))
(%auto)
(%qed)