All Questions
Tagged with inductive-type dependent-type
3
questions
2
votes
3
answers
247
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
4
votes
1
answer
179
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 ...
- 2,032
2
votes
0
answers
62
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