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: Jul 23 2024 at 21:01 UTC