def
Lean.Meta.kabstract
(e : Lean.Expr)
(p : Lean.Expr)
(occs : optParam Lean.Occurrences Lean.Occurrences.all)
:
Equations
- Lean.Meta.kabstract e p occs = do let e ← Lean.Meta.instantiateMVars e if (Lean.Expr.isFVar p && occs == Lean.Occurrences.all) = true then pure (Lean.Expr.abstract e #[p]) else let pHeadIdx := Lean.Expr.toHeadIndex p; let pNumArgs := Lean.Expr.headNumArgs p; (fun visit => StateRefT'.run' (visit e 0) 1) (Lean.Meta.kabstract.visit p occs pHeadIdx pNumArgs)
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)
: