Karl Palmskog (Oct 06 2021 at 08:33): Karl Palmskog (Oct 06 2021 at 08:33):is it possible/feasible to use the SSReflect rewrite tactic in a standalone fashion, e.g., by aliasing it to ssr_rewrite and mixing with the regular rewrite? If not directly, could one do it with some OCaml hacking?
Enrico Tassi (Oct 06 2021 at 08:35):FTR you can always access vanilla rewrite by using rewrite -> .... and rewrite <- ....
Karl Palmskog (Oct 06 2021 at 08:35):sure, but what I'm thinking of is the inverse scenario, we have a project that's "regular ltac", but we think the ssr rewrite might work better for us.
Enrico Tassi (Oct 06 2021 at 08:36):I guess one would need some OCaml hacking then.
Last updated: Nov 29 2023 at 18:01 UTC