Open DanielRrr opened 1 year ago
In Propositions and sets/Mere Proposition, there is the following example:
\func Unit-isProp : isProp Unit => \lam x y => idp
which is rejected with
[ERROR] Intro.ard:543:48: Expressions are not equal Left: x Right: y In: idp
I was using a freshly built version of the Arend Idea plugin.
Either the proof is wrong (but it doesn't seem so) or there is a bug in the typechecker.
In Propositions and sets/Mere Proposition, there is the following example:
which is rejected with
I was using a freshly built version of the Arend Idea plugin.
Either the proof is wrong (but it doesn't seem so) or there is a bug in the typechecker.