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

Equations

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

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

Equations

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

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

Equations

• info.getArity = info.paramInfo.size