All Questions
3
questions
2
votes
1
answer
40
views
Rewriting/Applying unidirectional morphisms in Coq
Link to Code Gist
I have the following definition
...
- 1,502
1
vote
1
answer
74
views
How do I enable this kind of rewriting?
Link to Code Gist
Given two extensionally equal sets, s1 ≡ s2, I want to be able to obtain a ∈ s2 from ...
- 1,502
4
votes
3
answers
444
views
Rewrite with definitional equality and dependent types
In Coq, there are some terms that are equal by definition, but there's not an easy way to replace one value with the other inside a proof. The two ways that I know that work in general are to use the ...
- 193