Stream: Coq users

Topic: Can I force `autorewrite` to use `setoid_rewrite`?


view this post on Zulip Yannick Forster (Dec 06 2021 at 12:13):

I have a rewrite based on eq which works with setoid_rewrite, but does not work with rewrite. I would like to put this as a hint into autorewrite, but since autorewrite uses rewrite when the underlying equality is eq the hint is not picked up. Can I somehow force autorewrite to use setoid_rewrite?

view this post on Zulip Yannick Forster (Dec 07 2021 at 09:07):

The answer seems to be "no". FTR, my workaround is to have Hint Extern 1 => autorewrite with db : db., call eauto with db instead of autorewrite with db and I add Hint Extern 1 => setoid_rewrite lemma : db. for rewrites that have to use setoid_rewrite


Last updated: Feb 01 2023 at 13:03 UTC