def Lean.Meta.getFunInfo (fn : Expr) (maxArgs? : Option Nat := none) : MetaM FunInfo

Equations

• Lean.Meta.getFunInfo fn maxArgs? = Lean.Meta.getFunInfoAux✝ fn maxArgs?

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