Documentation

Lean.Meta.FunInfo

source
def Lean.Meta.getFunInfo (fn : Expr) (maxArgs? : Option Nat := none) :
MetaM FunInfo
Equations
    Instances For
      source
      def Lean.Meta.getFunInfoNArgs (fn : Expr) (nargs : Nat) :
      MetaM FunInfo
      Equations
        Instances For
          source
          def Lean.Meta.FunInfo.getArity (info : FunInfo) :
          Nat
          Equations
            Instances For