inductive Lean.Meta.RecursorUnivLevelPos : Type

• motive: Lean.Meta.RecursorUnivLevelPos
• majorType: Nat → Lean.Meta.RecursorUnivLevelPos

instance Lean.Meta.instToStringRecursorUnivLevelPos : ToString Lean.Meta.RecursorUnivLevelPos

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Meta.RecursorInfo : Type

• recursorName : Lake.Name
• typeName : Lake.Name
• univLevelPos : List Lean.Meta.RecursorUnivLevelPos
• depElim : Bool
• recursive : Bool
• numArgs : Nat
• majorPos : Nat
• paramsPos : List (Option Nat)
• indicesPos : List Nat
• produceMotive : List Bool

def Lean.Meta.RecursorInfo.numParams (info : Lean.Meta.RecursorInfo) : Nat

Equations

• Lean.Meta.RecursorInfo.numParams info = List.length info.paramsPos

def Lean.Meta.RecursorInfo.numIndices (info : Lean.Meta.RecursorInfo) : Nat

Equations

• Lean.Meta.RecursorInfo.numIndices info = List.length info.indicesPos

def Lean.Meta.RecursorInfo.motivePos (info : Lean.Meta.RecursorInfo) : Nat

Equations

• Lean.Meta.RecursorInfo.motivePos info = Lean.Meta.RecursorInfo.numParams info

def Lean.Meta.RecursorInfo.firstIndexPos (info : Lean.Meta.RecursorInfo) : Nat

Equations

• Lean.Meta.RecursorInfo.firstIndexPos info = info.majorPos - Lean.Meta.RecursorInfo.numIndices info

def Lean.Meta.RecursorInfo.isMinor (info : Lean.Meta.RecursorInfo) (pos : Nat) : Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.RecursorInfo.numMinors (info : Lean.Meta.RecursorInfo) : Nat

Equations

• Lean.Meta.RecursorInfo.numMinors info = let r := info.numArgs; let r := r - Lean.Meta.RecursorInfo.motivePos info - 1; r - (info.majorPos + 1 - Lean.Meta.RecursorInfo.firstIndexPos info)

instance Lean.Meta.RecursorInfo.instToStringRecursorInfo : ToString Lean.Meta.RecursorInfo

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Attribute.Recursor.getMajorPos (stx : Lean.Syntax) : Lean.AttrM Nat

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Meta.recursorAttribute : Lean.ParametricAttribute Nat

def Lean.Meta.getMajorPos? (env : Lean.Environment) (declName : Lake.Name) : Option Nat

Equations

• Lean.Meta.getMajorPos? env declName = Lean.ParametricAttribute.getParam? Lean.Meta.recursorAttribute env declName

def Lean.Meta.mkRecursorInfo (declName : Lake.Name) (majorPos? : optParam (Option Nat) none) : Lean.MetaM Lean.Meta.RecursorInfo

Equations

• One or more equations did not get rendered due to their size.