All Questions
1
question
3
votes
2
answers
122
views
Is the validity of induction in Coq axiomatic?
When one defines an inductive type in Coq, for example, natural numbers,
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Coq automatically creates an ...
- 33