Questions tagged [natural-numbers]

For question about natural numbers $\Bbb N$, their properties and applications

Filter by
Sorted by
Tagged with
1 vote
1 answer

Strong induction for nat in Coq

I'm doing some exercises on Coq and trying to prove the strong induction principle for nat: ...
user avatar
13 votes
1 answer

Does the canonicity of natural number imply that of all types?

I've heard about a folklore claim that If all terms of ℕ are literals, all closed terms admit canonical form. In MLTT-style type theories. I am assured that it's true for Bool if one also assumes ...
user avatar