All Questions
Tagged with equality irrelevance
2
questions
1
vote
1
answer
83
views
Use proof irrelevance in cast
I'm working using cast in Coq.Vectors. When trying to rewrite with proofs, I'd like to use the fact of proof irrelevance (Coq.Logic.Eqdep_dec), preferably automatically. I.e., when I have a lemma ...
- 23
9
votes
2
answers
467
views
Defining coercion for proof irrelevant equality
Say I would like to define coercion for proof irrelevant equality between types. In Coq I try
...
- 2,290