abab9579 (Aug 27 2022 at 07:42): abab9579 (Aug 27 2022 at 07:42):Thank you!
Notification Bot (Aug 27 2022 at 07:43):abab9579 has marked this topic as resolved.
abab9579 (Sep 08 2022 at 08:18):Is there any references on /[1!Eq] pattern?
Ana de Almeida Borges (Sep 08 2022 at 11:23):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
Ana de Almeida Borges (Sep 08 2022 at 11:23):And yes, it's a view pattern that rewrites with Eq one time
abab9579 (Sep 08 2022 at 11:55):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!!
abab9579 (Sep 08 2022 at 11:57):Uh, how do I do this for reverse direction?
Enrico Tassi (Sep 08 2022 at 11:57):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.
Enrico Tassi (Sep 08 2022 at 11:59):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?
Enrico Tassi (Sep 08 2022 at 12:04):See also the proposal/discussion in https://github.com/math-comp/math-comp/pull/372
abab9579 (Sep 08 2022 at 12:11):I see, interesting. Thank you!
Last updated: Feb 08 2023 at 07:02 UTC