Documentation

Lean.Meta.RecursorInfo

source
inductive Lean.Meta.RecursorUnivLevelPos:
Type
source
instance Lean.Meta.instToStringRecursorUnivLevelPos:
ToString Lean.Meta.RecursorUnivLevelPos
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Meta.RecursorInfo:
Type
source
def Lean.Meta.RecursorInfo.numParams (info : Lean.Meta.RecursorInfo) :
Nat
Equations
source
def Lean.Meta.RecursorInfo.numIndices (info : Lean.Meta.RecursorInfo) :
Nat
Equations
source
def Lean.Meta.RecursorInfo.motivePos (info : Lean.Meta.RecursorInfo) :
Nat
Equations
source
def Lean.Meta.RecursorInfo.firstIndexPos (info : Lean.Meta.RecursorInfo) :
Nat
Equations
source
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.
source
def Lean.Meta.RecursorInfo.numMinors (info : Lean.Meta.RecursorInfo) :
Nat
Equations
source
instance Lean.Meta.RecursorInfo.instToStringRecursorInfo:
ToString Lean.Meta.RecursorInfo
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
opaque Lean.Meta.recursorAttribute:
Lean.ParametricAttribute Nat
source
def Lean.Meta.getMajorPos? (env : Lean.Environment) (declName : Lean.Name) :
Option Nat
Equations
source
def Lean.Meta.mkRecursorInfo (declName : Lean.Name) (majorPos? : optParam (Option Nat) none) :
Lean.MetaM Lean.Meta.RecursorInfo
Equations
  • One or more equations did not get rendered due to their size.