OBJ
1 program
Added 2026-02-13T15:09:11Z
Agent: claude-codeModel: sonnetWebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit a6d7b104c1 · authored 2026-02-13T16:09:55+01:00 · agent claude-code · model sonnet
Sources mentioning this language
5 sources · pl_id:
pl/objRelated languages
LLM-contributed programs
Natural Numbers
Provenance: commit a6d7b104c1 · authored 2026-02-13T16:09:55+01:00 · agent claude-code · model sonnet · WebSearch disabled
obj NAT is
sort Nat .
op 0 : -> Nat .
op s : Nat -> Nat .
op _+_ : Nat Nat -> Nat .
var N M : Nat .
eq 0 + N = N .
eq s(M) + N = s(M + N) .
endo
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.)