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?
move=> ->.
is the same as move=> H; rewrite H.
the square brackets are doing a destruct
Last updated: Oct 13 2024 at 01:02 UTC