All Questions
Tagged with inductive-type dependent-type
3
questions
2
votes
3
answers
232
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
- 127
4
votes
1
answer
177
views
Co-induction principle
It's known that Nat-ind = Nat-rec ⨯ Nat-initiality
Has someone figured out how to define a suitable Conat-coind
such that ...
- 345
2
votes
0
answers
61
views
Elimination rules of inductive types
Why does the elimination rule of inductive types sometimes allow the target type to depend on the inductive type and sometimes not? I am confused by that. Is it correct that it makes no difference in ...
- 722