Stream: math-comp users

Topic: Few syntax doubts


view this post on Zulip Julin Shaji (Oct 23 2023 at 17:06):

Hi. I was reading the mathcomp book (not linearly, but from here and there) and couldn't understand some of the syntax. Could someone help me understand it?

This was one of them:

Lemma example a b : a && b ==> (a == b).
Proof. by case: andP => [[-> ->] |]. Qed.

What does the [-> ->] mean here?

view this post on Zulip Ana de Almeida Borges (Oct 23 2023 at 21:58):

move=> ->. is the same as move=> H; rewrite H.

view this post on Zulip Ana de Almeida Borges (Oct 23 2023 at 21:58):

the square brackets are doing a destruct


Last updated: Oct 13 2024 at 01:02 UTC