Stream: Coq users

Topic: Subst for setoids?

view this post on Zulip Roger Bosman (May 05 2021 at 10:33):

Hi all, substs eliminates hypotheses of form x = y by rewriting all occurances and then discharging the hypothesis. However, this does not work for alternate equivalence relations. Is there a setoid-based (?) variant that does this?

view this post on Zulip MackieLoeffel (May 05 2021 at 12:04):

std++ has a setoid_subst tactic that may do what you want (for the std++ equiv relation):

Last updated: Jul 23 2024 at 17:01 UTC