Stream: Coq users

Topic: JMeq discriminate

view this post on Zulip Julien Blond (Apr 12 2022 at 16:06):

Hi ! How can I discriminate equalities like

Heq_l : Nnil ~= Ncons x l

where Nnil and Ncons are dependent list constructors ?

view this post on Zulip Gaëtan Gilbert (Apr 12 2022 at 17:18):

what's ~=

view this post on Zulip Karl Palmskog (Apr 12 2022 at 18:38):

I think this is the one, in Program.Equality:

Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).

view this post on Zulip Karl Palmskog (Apr 12 2022 at 18:41):

one way to work with assumptions that use JMeq is to apply JMeq_eq (uses axiom Eqdep.Eq_rect_eq.eq_rect_eq on recent Coq), then they become a normal equality.

view this post on Zulip Li-yao (Apr 12 2022 at 18:53):

It seems not sufficient in this case because both sides don't have the same type for JMeq_eq to be applicable.

Last updated: Dec 06 2023 at 15:01 UTC