Stream: Coq users

Topic: replacing with ssr rewrite


view this post on Zulip Karl Palmskog (Aug 07 2023 at 14:05):

What is the recommended incantation for using the SSReflect rewrite tactic and as little as possible of anything else from SSReflect? In the refman, I find this:

From Coq Require ssreflect.
Import ssreflect.SsrSyntax.

but is using "just this" recommended/viable?

Context: it was discussed at the Coq Workshop last week that people having unintuitive unification issues may want to just use the ssr rewrite as a drop-in replacement for regular rewrite.

view this post on Zulip Karl Palmskog (Aug 08 2023 at 11:56):

@Enrico Tassi any chance for an "official" recommendation here?

view this post on Zulip Enrico Tassi (Aug 08 2023 at 11:59):

I have not tested it in a while, but if it still works, that would be it.

view this post on Zulip Karl Palmskog (Aug 08 2023 at 12:00):

thanks, I'll try to test then


Last updated: Jun 22 2024 at 15:01 UTC