source
def Lean.Meta.kabstract (e p : Expr) (occs : Occurrences := Occurrences.all) :
MetaM Expr

Abstract occurrences of `p` in `e`. We detect subterms equivalent to `p` using key-matching. That is, only perform `isDefEq` tests when the head symbol of subterm is equivalent to head symbol of `p`.

By default, all occurrences are abstracted, but this behavior can be controlled using the `occs` parameter.

All matches of `p` in `e` are considered for occurrences, but for each match that is included by the `occs` parameter, metavariables appearing in `p` (or `e`) may become instantiated, affecting the possibility of subsequent matches. For matches that are not included in the `occs` parameter, the metavariable context is rolled back to prevent blocking subsequent matches which require different instantiations.

Equations

- One or more equations did not get rendered due to their size.

Instances For