Yannick Forster (Dec 06 2021 at 12:13): 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?
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: Oct 05 2023 at 02:01 UTC