Documentation
Lean
.
Meta
.
FunInfo
Search
return to top
source
Imports
Lean.Meta.Basic
Lean.Meta.InferType
Imported by
Lean
.
Meta
.
getFunInfo
Lean
.
Meta
.
getFunInfoNArgs
Lean
.
Meta
.
FunInfo
.
getArity
source
def
Lean
.
Meta
.
getFunInfo
(
fn
:
Expr
)
:
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