Thank you!

abab9579 has marked this topic as resolved.

Is there any references on `/[1!Eq]`

pattern?

It's not in Coq yet (at least not in 8.15), only in mathcomp. So you wouldn't find it in the Coq refman. There is a brief explanation in the math-comp version of the ssreflect.v file: https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssreflect.html

And yes, it's a view pattern that rewrites with `Eq`

one time

I thought all ssreflect tactics would be at https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html?highlight=ssreflect#grammar-token-occ_switch . I guess there is more. Anyway, thank you!!

Uh, how do I do this for reverse direction?

That thing is user-defined, see https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#views the `ltac:(...)`

. It can't be in Coq's manual, since it is defined in MC.

```
Module Export ipat.
Notation "'[' '1' '!' rules ']'" := (ltac:(rewrite rules))
(at level 0, rules at level 200, only parsing) : ssripat_scope.
Notation "'[' '!' rules ']'" := (ltac:(rewrite !rules))
(at level 0, rules at level 200, only parsing) : ssripat_scope.
End ipat.
```

I see. Oh, so this is just a concise notation. I guess I could have another notation for myself for reverse direction?

See also the proposal/discussion in https://github.com/math-comp/math-comp/pull/372

I see, interesting. Thank you!

Last updated: Feb 08 2023 at 07:02 UTC