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?
FTR you can always access vanilla rewrite by using
rewrite -> .... and
rewrite <- ....
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.
I guess one would need some OCaml hacking then.
Last updated: Feb 09 2023 at 02:02 UTC