def Lean.Meta.getFunInfo (fn : Lean.Expr) : Lean.MetaM Lean.Meta.FunInfo

Equations

• Lean.Meta.getFunInfo fn = Lean.Meta.getFunInfoAux✝ fn none

def Lean.Meta.getFunInfoNArgs (fn : Lean.Expr) (nargs : Nat) : Lean.MetaM Lean.Meta.FunInfo

Equations

• Lean.Meta.getFunInfoNArgs fn nargs = Lean.Meta.getFunInfoAux✝ fn (some nargs)

def Lean.Meta.FunInfo.getArity (info : Lean.Meta.FunInfo) : Nat

Equations

• info.getArity = info.paramInfo.size