def
Lean.Meta.kabstract
(e : Lean.Expr)
(p : Lean.Expr)
(occs : optParam Lean.Occurrences Lean.Occurrences.all)
:
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.
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Meta.kabstract.visit
(p : Lean.Expr)
(occs : optParam Lean.Occurrences Lean.Occurrences.all)
(pHeadIdx : Lean.HeadIndex)
(pNumArgs : Nat)
(e : Lean.Expr)
(offset : Nat)
: