inductive Lean.Meta.RecursorUnivLevelPos : Type

• motive : RecursorUnivLevelPos
• majorType (idx : Nat) : RecursorUnivLevelPos

Instances For

• Lean.Meta.instToStringRecursorUnivLevelPos

instance Lean.Meta.instToStringRecursorUnivLevelPos : ToString RecursorUnivLevelPos

Equations

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

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

• Lean.Meta.RecursorInfo.instToString

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

Equations

• info.numParams = info.paramsPos.length

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

Equations

• info.numIndices = info.indicesPos.length

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

Equations

• info.motivePos = info.numParams

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

Equations

• info.firstIndexPos = info.majorPos - info.numIndices

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

Equations

• info.isMinor pos = if pos ≤ info.motivePos then false else if (decide (info.firstIndexPos ≤ pos) && decide (pos ≤ info.majorPos)) = true then false else true

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

Equations

• info.numMinors = info.numArgs - info.motivePos - 1 - (info.majorPos + 1 - info.firstIndexPos)

instance Lean.Meta.RecursorInfo.instToString : ToString RecursorInfo

Equations

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

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

Equations

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

opaque Lean.Meta.recursorAttribute : ParametricAttribute Nat

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

Equations

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

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

Equations

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