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

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

Instances For

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

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

Instances For

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

- info.getArity = info.paramInfo.size

Instances For