Skip to content

[ fix #385 ] Implement predNat primitive - #459

Merged
jespercockx merged 1 commit into
agda:masterfrom
jespercockx:issue385
Aug 5, 2026
Merged

[ fix #385 ] Implement predNat primitive#459
jespercockx merged 1 commit into
agda:masterfrom
jespercockx:issue385

Conversation

@jespercockx

Copy link
Copy Markdown
Member

This just implements my original suggestion of having a primitive predecessor rather than trying to compile pattern matching in a smarter way.

AI disclosure: this was generated by GLM-5.2 running on renewable energy in the EU (shoot me).

@jespercockx jespercockx linked an issue Aug 5, 2026 that may be closed by this pull request
@jespercockx
jespercockx merged commit ca91a75 into agda:master Aug 5, 2026
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Add predecessor for natural numbers

1 participant