Documentation

Lean.Meta.RecursorInfo

inductive Lean.Meta.RecursorUnivLevelPos :

Type

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

instance Lean.Meta.instToStringRecursorUnivLevelPos :

ToString Lean.Meta.RecursorUnivLevelPos

Equations

Lean.Meta.instToStringRecursorUnivLevelPos = { toString := fun x => match x with | Lean.Meta.RecursorUnivLevelPos.motive => "" | Lean.Meta.RecursorUnivLevelPos.majorType idx => toString idx }

structure Lean.Meta.RecursorInfo :

Type

recursorName : Lean.Name
typeName : Lean.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) :

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Lean.Meta.RecursorInfo.instToStringRecursorInfo = { toString := fun info => "{\n" ++ " name := " ++ toString info.recursorName ++ "\n" ++ " type := " ++ toString info.typeName ++ "\n" ++ " univs := " ++ toString info.univLevelPos ++ "\n" ++ " depElim := " ++ toString info.depElim ++ "\n" ++ " recursive := " ++ toString info.recursive ++ "\n" ++ " numArgs := " ++ toString info.numArgs ++ "\n" ++ " numParams := " ++ toString (Lean.Meta.RecursorInfo.numParams info) ++ "\n" ++ " numIndices := " ++ toString (Lean.Meta.RecursorInfo.numIndices info) ++ "\n" ++ " numMinors := " ++ toString (Lean.Meta.RecursorInfo.numMinors info) ++ "\n" ++ " major := " ++ toString info.majorPos ++ "\n" ++ " motive := " ++ toString (Lean.Meta.RecursorInfo.motivePos info) ++ "\n" ++ " paramsAtMajor := " ++ toString info.paramsPos ++ "\n" ++ " indicesAtMajor := " ++ toString info.indicesPos ++ "\n" ++ " produceMotive := " ++ toString info.produceMotive ++ "\n" ++ "}" }

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

Equations

Lean.Meta.Attribute.Recursor.getMajorPos stx = if (Lean.Syntax.getKind stx == `Lean.Parser.Attr.recursor) = true then let pos := Option.getD (Lean.Syntax.isNatLit? (Lean.Syntax.getOp stx 1)) 0; let _do_jp := fun y => pure (pos - 1); if (pos == 0) = true then do let y ← Lean.throwErrorAt stx (Lean.toMessageData "major premise position must be greater than zero") _do_jp y else do let y ← pure PUnit.unit _do_jp y else Lean.throwErrorAt stx (Lean.toMessageData "unexpected attribute argument, numeral expected")

constant Lean.Meta.recursorAttribute :

Lean.ParametricAttribute Nat

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

Equations

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

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

Lean.MetaM Lean.Meta.RecursorInfo

Equations

Lean.Meta.mkRecursorInfo declName majorPos? = do let cinfo ← Lean.getConstInfo declName match cinfo with | Lean.ConstantInfo.recInfo val => Lean.Meta.mkRecursorInfoForKernelRec declName val | x => match majorPos? with | none => do let a ← Lean.getEnv Lean.Meta.mkRecursorInfoAux cinfo (Lean.Meta.getMajorPos? a declName) | x => Lean.Meta.mkRecursorInfoAux cinfo majorPos?