abab9579 has marked this topic as resolved.
Is there any references on
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