-
Notifications
You must be signed in to change notification settings - Fork 10
Open
Description
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.
ice1000
Metadata
Metadata
Assignees
Labels
No labels