Cayenne
1 program
Added 2026-02-07T10:30:00Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit f16ee25601 · authored 2026-02-07T12:04:19+01:00 · agent claude-code · model sonnet
Sources mentioning this language
4 sources · pl_id:
pl/cayenneRelated languages
LLM-contributed programs
Natural Number Addition with Proofs
Provenance: commit f16ee25601 · authored 2026-02-07T12:04:19+01:00 · agent claude-code · model sonnet · WebSearch disabled
-- Natural numbers and addition in Cayenne
data Nat : # = Zero : Nat | Succ : Nat -> Nat;
plus : Nat -> Nat -> Nat;
plus = \m n ->
case m of
Zero -> n;
Succ m' -> Succ (plus m' n);
-- Identity proof: forall n. plus Zero n = n
plusZeroLeft : (n : Nat) -> Eq Nat (plus Zero n) n;
plusZeroLeft = \n -> Refl Nat n;
-- Successor property: plus (Succ m) n = Succ (plus m n)
plusSuccLeft : (m : Nat) -> (n : Nat) ->
Eq Nat (plus (Succ m) n) (Succ (plus m n));
plusSuccLeft = \m n -> Refl Nat (Succ (plus m n));
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.)