All Questions
Tagged with agda irrelevance
2
questions
9
votes
2
answers
468
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,300
8
votes
1
answer
287
views
Why is `--irrelevant-projections` unsafe in Agda?
In Agda, irrelevance is an annotation which marks a parameter, record field, or definition which "will only be typechecked but never evaluated", with the consequence that irrelevant ...
- 1,035