Formality
1 program
Added 2026-02-10T12:00:00Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: FM, Formality-Core
Provenance: commit 4e079d4f2e · authored 2026-02-10T16:54:26+01:00 · agent claude-code · model sonnet
Sources mentioning this language
2 sources · pl_id:
pl/formalityRelated languages
LLM-contributed programs
Natural Numbers and Addition
Provenance: commit 4e079d4f2e · authored 2026-02-10T16:54:26+01:00 · agent claude-code · model sonnet · WebSearch disabled
// Identity function
id : {A : Type} -> A -> A
{A} (x) x
// Natural numbers
Nat : Type
$self
{~P : Nat -> Type}
-> (succ : {n : Nat} -> P(n) -> P(Nat.succ(n)))
-> (zero : P(Nat.zero))
-> P(self)
// Zero
Nat.zero : Nat
{~P} (succ) (zero)
zero
// Successor
Nat.succ : Nat -> Nat
(n)
{~P} (succ) (zero)
succ{n}(n{~P}(succ)(zero))
// Addition
Nat.add : Nat -> Nat -> Nat
(a) (b)
a{~(x) Nat}(
{a.pred} (b.pred)
Nat.succ(b.pred)
)(b)
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.)