Documentation

Lean.Meta.KAbstract

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 substerm 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
    Instances For
      def Lean.Meta.kabstract.visit (p : Expr) (occs : Occurrences := Occurrences.all) (pHeadIdx : HeadIndex) (pNumArgs : Nat) (e : Expr) (offset : Nat) :
      Equations
        Instances For