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...


Last updated: Jan 29 2023 at 19:02 UTC