Laurent Théry (May 04 2022 at 14:52): Laurent Théry (May 04 2022 at 14:52):I usually try to turn my case: T into have [] := T but this does not work here I don't why.
This works
Goal forall x1 x2 : nat,
match x1 =P x2 with ReflectT _ => True | ReflectF _ => False end.
move=> x1 x2.
case: (x1 =P x2).
This does not work
Goal forall x1 x2 : nat,
match x1 =P x2 with ReflectT _ => True | ReflectF _ => False end.
move=> x1 x2.
have [] := x1 =P x2.
what am I missing?
Paolo Giarrusso (May 04 2022 at 20:32):I'd expect the first one destructs the occurrence of your T in the context, while have isn't supposed to do that...
Last updated: Jan 29 2023 at 19:02 UTC