Stream: Coq users

Topic: Possible to deactivate `rewrite = setoid_rewrite`?


view this post on Zulip Pierre Rousselin (Jan 15 2024 at 18:08):

For teaching at a basic level, the fact that rewrite behaves as setoid_rewrite whenever some required library has Required Setoid can be a problem:

Is there a way to fall back to vanilla rewrite even if Setoid has beenRequired?

view this post on Zulip Gaëtan Gilbert (Jan 15 2024 at 20:19):

no
also I think rewrite at is always setoid_rewrite

view this post on Zulip Matthieu Sozeau (Feb 05 2024 at 17:18):

It should be easy to optionally disable this behavior though


Last updated: Jun 23 2024 at 04:03 UTC