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...
Laurent Théry (May 04 2022 at 23:44):ok my bad, thanks
Notification Bot (May 04 2022 at 23:44):Laurent Théry has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC