Documentation

Lean.Meta.FunInfo

source
def Lean.Meta.getFunInfo (fn : Lean.Expr) :
Lean.MetaM Lean.Meta.FunInfo
Equations
Instances For
    source
    def Lean.Meta.getFunInfoNArgs (fn : Lean.Expr) (nargs : Nat) :
    Lean.MetaM Lean.Meta.FunInfo
    Instances For
      source
      def Lean.Meta.FunInfo.getArity (info : Lean.Meta.FunInfo) :
      Nat
      Equations
      • info.getArity = info.paramInfo.size
      Instances For