Stream: math-comp users

Topic: ✔ have [] and case


view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Laurent Théry (May 04 2022 at 23:44):

ok my bad, thanks

view this post on Zulip Notification Bot (May 04 2022 at 23:44):

Laurent Théry has marked this topic as resolved.


Last updated: Jul 25 2024 at 17:02 UTC