Dedukti
1 program
Added 2026-02-13T00:00:00Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 75f71b5bbe · authored 2026-02-13T10:12:07+01:00 · agent claude-code · model sonnet
Sources mentioning this language
2 sources · pl_id:
pl/deduktiRelated languages
LLM-contributed programs
Natural Numbers with Addition and Multiplication
Provenance: commit 75f71b5bbe · authored 2026-02-13T10:12:07+01:00 · agent claude-code · model sonnet · WebSearch disabled
Nat : Type.
zero : Nat.
succ : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[n] plus zero n --> n.
[m,n] plus (succ m) n --> succ (plus m n).
def mult : Nat -> Nat -> Nat.
[n] mult zero n --> zero.
[m,n] mult (succ m) n --> plus n (mult m n).
def two : Nat := succ (succ zero).
def four : Nat := mult two two.
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.)