Joshua Grosso (Sep 20 2020 at 00:59): Joshua Grosso (Sep 20 2020 at 00:59):Is there a way to run replace foo with bar if foo has holes? (e.g. if foo is (_ + 1) and the goal contains a subterm of the form (<something> + 1), I would like that subterm to be replaced with bar.)
Joshua Grosso (Sep 20 2020 at 02:38):Hmm, seems SSReflect's pattern-matching-replace functionality might be what I'm looking for.
Cyril Cohen (Sep 21 2020 at 16:26):Joshua Grosso said:
Hmm, seems SSReflect's pattern-matching-replace functionality might be what I'm looking for.
Indeed, after you load ssreflect you can write rewrite -[pattern with holes]/(replacement with holes).
Last updated: Sep 30 2023 at 06:01 UTC