Stream: Coq users

Topic: Elaborator limitation


view this post on Zulip Yann Leray (Feb 21 2024 at 16:46):

Not a bug per se, but I'm surprised that the following fails :

Check match tt with _ => eq_refl end.

view this post on Zulip Meven Lennon-Bertrand (Feb 21 2024 at 17:05):

Why is that? What would you expect Coq to fill in for the (implicit) parameter of eq_refl?

view this post on Zulip Yann Leray (Feb 21 2024 at 17:07):

I would expect it to have type @eq ?T@{c := tt} ?a@{c := tt} ?a@{c := tt}, but the heuristic cannot identify the two last arguments of eq since they have nonempty instantiation, or so I understand.


Last updated: Jun 22 2024 at 15:01 UTC