opaque Lean.Elab.Command.inductive.autoPromoteIndices : Lean.Option Bool

def Lean.Elab.Command.checkValidInductiveModifier {m : Type → Type} [Monad m] [Lean.MonadError m] (modifiers : Lean.Elab.Modifiers) : m Unit

Equations

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

def Lean.Elab.Command.checkValidCtorModifier {m : Type → Type} [Monad m] [Lean.MonadError m] (modifiers : Lean.Elab.Modifiers) : m Unit

Equations

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

structure Lean.Elab.Command.CtorView : Type

• ref : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• declName : Lean.Name
• binders : Lean.Syntax
• type? : Option Lean.Syntax

Instances For

• Lean.Elab.Command.instInhabitedCtorView

instance Lean.Elab.Command.instInhabitedCtorView : Inhabited Lean.Elab.Command.CtorView

Equations

• Lean.Elab.Command.instInhabitedCtorView = { default := { ref := default, modifiers := default, declName := default, binders := default, type? := default } }

structure Lean.Elab.Command.ComputedFieldView : Type

• ref : Lean.Syntax
• modifiers : Lean.Syntax
• fieldId : Lean.Name
• type : Lean.Term
• matchAlts : Lean.TSyntax `Lean.Parser.Term.matchAlts

structure Lean.Elab.Command.InductiveView : Type

• ref : Lean.Syntax
• declId : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• shortDeclName : Lean.Name
• declName : Lean.Name
• levelNames : List Lean.Name
• binders : Lean.Syntax
• type? : Option Lean.Syntax
• ctors : Array Lean.Elab.Command.CtorView
• derivingClasses : Array Lean.Elab.DerivingClassView
• computedFields : Array Lean.Elab.Command.ComputedFieldView

Instances For

• Lean.Elab.Command.instInhabitedInductiveView

instance Lean.Elab.Command.instInhabitedInductiveView : Inhabited Lean.Elab.Command.InductiveView

Equations

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

structure Lean.Elab.Command.ElabHeaderResult : Type

• view : Lean.Elab.Command.InductiveView
• lctx : Lean.LocalContext
• localInsts : Lean.LocalInstances
• levelNames : List Lean.Name
• params : Array Lean.Expr
• type : Lean.Expr

Instances For

• Lean.Elab.Command.instInhabitedElabHeaderResult

instance Lean.Elab.Command.instInhabitedElabHeaderResult : Inhabited Lean.Elab.Command.ElabHeaderResult

Equations

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

def Lean.Elab.Command.shouldInferResultUniverse (u : Lean.Level) : Lean.Elab.TermElabM (Option Lean.LMVarId)

Return some ?m if u is of the form ?m + k. Return none if u does not contain universe metavariables. Throw exception otherwise.

Equations

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

def Lean.Elab.Command.mkResultUniverse (us : Array Lean.Level) (rOffset : Nat) (preferProp : Bool) : Lean.Level

Equations

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

def Lean.Elab.Command.accLevel (u r : Lean.Level) (rOffset : Nat) : OptionT (StateT (Array Lean.Level) Id) Unit

Auxiliary function for updateResultingUniverse accLevel u r rOffset add u to state if it is not already there and it is different from the resulting universe level r+rOffset.

If u is a max, then its components are recursively processed. If u is a succ and rOffset > 0, we process the us child using rOffset-1.

This method is used to infer the resulting universe level of an inductive datatype.

Equations

• Lean.Elab.Command.accLevel u r rOffset = Lean.Elab.Command.accLevel.go r u rOffset

def Lean.Elab.Command.accLevel.go (r u : Lean.Level) (rOffset : Nat) : OptionT (StateT (Array Lean.Level) Id) Unit

def Lean.Elab.Command.accLevelAtCtor (ctor : Lean.Constructor) (ctorParam : Lean.Expr) (r : Lean.Level) (rOffset : Nat) : StateRefT' IO.RealWorld (Array Lean.Level) Lean.Elab.TermElabM Unit

Auxiliary function for updateResultingUniverse accLevelAtCtor ctor ctorParam r rOffset add u (ctorParam's universe) to state if it is not already there and it is different from the resulting universe level r+rOffset.

See accLevel.

Equations

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

def Lean.Elab.Command.withCtorRef {m : Type → Type} {α : Type} [Monad m] [Lean.MonadRef m] (views : Array Lean.Elab.Command.InductiveView) (ctorName : Lean.Name) (k : m α) : m α

Execute k using the Syntax reference associated with constructor ctorName.

Equations

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

opaque Lean.Elab.Command.bootstrap.inductiveCheckResultingUniverse : Lean.Option Bool

def Lean.Elab.Command.checkResultingUniverse (u : Lean.Level) : Lean.Elab.TermElabM Unit

Equations

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

def Lean.Elab.Command.elabInductiveViews (vars : Array Lean.Expr) (views : Array Lean.Elab.Command.InductiveView) : Lean.Elab.TermElabM Unit

Equations

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

def Lean.Elab.Command.elabInductiveViewsPostprocessing (views : Array Lean.Elab.Command.InductiveView) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Lean.Elab.Command.elabInductives (inductives : Array (Lean.Elab.Modifiers × Lean.Syntax)) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Lean.Elab.Command.elabInductive (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

Equations

• Lean.Elab.Command.elabInductive modifiers stx = Lean.Elab.Command.elabInductives #[(modifiers, stx)]

def Lean.Elab.Command.elabClassInductive (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

Equations

• Lean.Elab.Command.elabClassInductive modifiers stx = Lean.Elab.Command.elabInductive (modifiers.addAttr { kind := Lean.AttributeKind.global, name := `class, stx := Lean.Syntax.missing }) stx

def Lean.Elab.Command.isMutualInductive (stx : Lean.Syntax) : Bool

Returns true if all elements of the mutual block (Lean.Parser.Command.mutual) are inductive declarations.

Equations

• Lean.Elab.Command.isMutualInductive stx = stx[1].getArgs.all fun (elem : Lean.Syntax) => let decl := elem[1]; let declKind := decl.getKind; declKind == `Lean.Parser.Command.inductive

def Lean.Elab.Command.elabMutualInductive (elems : Array Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

Elaborates a mutual block satisfying Lean.Elab.Command.isMutualInductive.

Equations

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