Stream: Coq users

Topic: `replace` with holes


view this post on Zulip 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.)

view this post on Zulip Joshua Grosso (Sep 20 2020 at 02:38):

Hmm, seems SSReflect's pattern-matching-replace functionality might be what I'm looking for.

view this post on Zulip 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: Jan 29 2023 at 05:03 UTC