Documentation

Lean.Meta.KAbstract

source
def Lean.Meta.kabstract (e : Lean.Expr) (p : Lean.Expr) (occs : optParam Lean.Occurrences Lean.Occurrences.all) :
Lean.MetaM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
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) :
StateRefT' IO.RealWorld Nat Lean.MetaM Lean.Expr