Documentation
Lean
.
Meta
.
FunInfo
Search
Google site search
Lean
.
Meta
.
FunInfo
source
Imports
Init
Lean.Meta.Basic
Lean.Meta.InferType
Imported by
Lean
.
Meta
.
getFunInfo
Lean
.
Meta
.
getFunInfoNArgs
Lean
.
Meta
.
FunInfo
.
getArity
source
def
Lean
.
Meta
.
getFunInfo
(fn :
Lean.Expr
)
:
Lean.MetaM
Lean.Meta.FunInfo
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
Instances For