Kind2
1 program
Added 2026-02-12T09:11:42Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: Kind 2
Provenance: commit bb62aaff0c · authored 2026-02-12T10:12:19+01:00 · agent claude-code · model sonnet
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Natural Number Addition with Commutativity Proof
Provenance: commit bb62aaff0c · authored 2026-02-12T10:12:19+01:00 · agent claude-code · model sonnet · WebSearch disabled
// Proof of addition commutativity
Nat.add.comm (a: Nat) (b: Nat) : (Nat.add a b) == (Nat.add b a)
Nat.add.comm Nat.zero b = ?comm_zero
Nat.add.comm (Nat.succ a) b = ?comm_succ
// Natural numbers
type Nat {
zero
succ (pred: Nat)
}
// Addition function
Nat.add (a: Nat) (b: Nat) : Nat
Nat.add Nat.zero b = b
Nat.add (Nat.succ a) b = Nat.succ (Nat.add a b)
// Main function
Main : Nat {
Nat.add (Nat.succ (Nat.succ Nat.zero)) (Nat.succ (Nat.succ (Nat.succ Nat.zero)))
}