-
Notifications
You must be signed in to change notification settings - Fork 34
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Is that a problem of variable inference? #236
Comments
I guess it tries to unify the two sides without trying to compute one of them. |
Can't you just write
? |
That's not related to this inference problem. The proof can be simplified, and I'm aware of that |
Even |
Anyway, the problem is |
I have a proof that type-checks:
I'm using a
lemma
whose type is whatever but the body isidp
, which means its lhs and rhs are convertible.However, when I inline
lemma
, say, replace it withidp
directly, Arend gives me type error.Why should this happen?
The does-not-work code:
The error message:
The text was updated successfully, but these errors were encountered: