Documentation
Lean
.
Meta
.
RecursorInfo
Search
return to top
source
Imports
Lean.AuxRecursor
Lean.Meta.Basic
Lean.Util.FindExpr
Imported by
Lean
.
Meta
.
RecursorUnivLevelPos
Lean
.
Meta
.
instToStringRecursorUnivLevelPos
Lean
.
Meta
.
RecursorInfo
Lean
.
Meta
.
RecursorInfo
.
numParams
Lean
.
Meta
.
RecursorInfo
.
numIndices
Lean
.
Meta
.
RecursorInfo
.
motivePos
Lean
.
Meta
.
RecursorInfo
.
firstIndexPos
Lean
.
Meta
.
RecursorInfo
.
isMinor
Lean
.
Meta
.
RecursorInfo
.
numMinors
Lean
.
Meta
.
RecursorInfo
.
instToString
Lean
.
Meta
.
Attribute
.
Recursor
.
getMajorPos
Lean
.
Meta
.
recursorAttribute
Lean
.
Meta
.
getMajorPos?
Lean
.
Meta
.
mkRecursorInfo
source
inductive
Lean
.
Meta
.
RecursorUnivLevelPos
:
Type
motive :
RecursorUnivLevelPos
majorType
(
idx
:
Nat
)
:
RecursorUnivLevelPos
Instances For
source
instance
Lean
.
Meta
.
instToStringRecursorUnivLevelPos
:
ToString
RecursorUnivLevelPos
Equations
source
structure
Lean
.
Meta
.
RecursorInfo
:
Type
recursorName :
Name
typeName :
Name
univLevelPos :
List
RecursorUnivLevelPos
depElim :
Bool
recursive :
Bool
numArgs :
Nat
majorPos :
Nat
paramsPos :
List
(
Option
Nat
)
indicesPos :
List
Nat
produceMotive :
List
Bool
Instances For
source
def
Lean
.
Meta
.
RecursorInfo
.
numParams
(
info
:
RecursorInfo
)
:
Nat
Equations
Instances For
source
def
Lean
.
Meta
.
RecursorInfo
.
numIndices
(
info
:
RecursorInfo
)
:
Nat
Equations
Instances For
source
def
Lean
.
Meta
.
RecursorInfo
.
motivePos
(
info
:
RecursorInfo
)
:
Nat
Equations
Instances For
source
def
Lean
.
Meta
.
RecursorInfo
.
firstIndexPos
(
info
:
RecursorInfo
)
:
Nat
Equations
Instances For
source
def
Lean
.
Meta
.
RecursorInfo
.
isMinor
(
info
:
RecursorInfo
)
(
pos
:
Nat
)
:
Bool
Equations
Instances For
source
def
Lean
.
Meta
.
RecursorInfo
.
numMinors
(
info
:
RecursorInfo
)
:
Nat
Equations
Instances For
source
instance
Lean
.
Meta
.
RecursorInfo
.
instToString
:
ToString
RecursorInfo
Equations
source
def
Lean
.
Meta
.
Attribute
.
Recursor
.
getMajorPos
(
stx
:
Syntax
)
:
AttrM
Nat
Equations
Instances For
source
opaque
Lean
.
Meta
.
recursorAttribute
:
ParametricAttribute
Nat
source
def
Lean
.
Meta
.
getMajorPos?
(
env
:
Environment
)
(
declName
:
Name
)
:
Option
Nat
Equations
Instances For
source
def
Lean
.
Meta
.
mkRecursorInfo
(
declName
:
Name
)
(
majorPos?
:
Option
Nat
:=
none
)
:
MetaM
RecursorInfo
Equations
Instances For