Stream: math-comp devs

Topic: ssr rewrite tactic standalone


view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Oct 06 2021 at 08:35):

FTR you can always access vanilla rewrite by using rewrite -> .... and rewrite <- ....

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 06 2021 at 08:36):

I guess one would need some OCaml hacking then.


Last updated: Mar 28 2024 at 20:01 UTC