Stream: Coq users

Topic: Possible to deactivate `rewrite = setoid_rewrite`?

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:

• rewrite can be used in many situations where it should not (e.g. rewrite using an inequality, or anything really)
• then the error messages can be very confusing
• finally, it can be important to use different names for, say, reasoning by equivalence and reasoning with equalities

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

Gaëtan Gilbert (Jan 15 2024 at 20:19):

no
also I think rewrite at is always setoid_rewrite

Matthieu Sozeau (Feb 05 2024 at 17:18):

It should be easy to optionally disable this behavior though

Last updated: Oct 13 2024 at 01:02 UTC