def Lean.Elab.Command.checkValidInductiveModifier {m : Type → Type} [inst : Monad m] [inst : 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} [inst : Monad m] [inst : 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

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.Name.mkStr4 "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

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
• params : Array Lean.Expr
• type : Lean.Expr

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

Equations

• Lean.Elab.Command.instInhabitedElabHeaderResult = { default := { view := default, lctx := default, localInsts := default, params := default, type := default } }

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) : Lean.Level

Equations

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

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.

Equations

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

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.

Equations

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

def Lean.Elab.Command.withCtorRef {m : Type → Type} {α : Type} [inst : Monad m] [inst : 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 (views : Array Lean.Elab.Command.InductiveView) : Lean.Elab.Command.CommandElabM Unit

Equations

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