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

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

structure Lean.Elab.Command.CtorView : Type

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

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

structure Lean.Elab.Command.ComputedFieldView : Type

• ref : Lean.Syntax
• modifiers : Lean.Syntax
• fieldId : Lake.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 : Lake.Name
• declName : Lake.Name
• levelNames : List Lake.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

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

structure Lean.Elab.Command.ElabHeaderResult : Type

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

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

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.

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

def Lean.Elab.Command.accLevel (u : Lean.Level) (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.

def Lean.Elab.Command.accLevel.go (r : Lean.Level) (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.

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

Execute k using the Syntax reference associated with constructor ctorName.

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

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

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