# Documentation

Lean.Elab.Inductive

def Lean.Elab.Command.checkValidInductiveModifier {m : } [inst : ] [inst : ] (modifiers : Lean.Elab.Modifiers) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Command.checkValidCtorModifier {m : } [inst : ] [inst : ] (modifiers : Lean.Elab.Modifiers) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations

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

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
def Lean.Elab.Command.accLevelAtCtor (ctor : Lean.Constructor) (ctorParam : Lean.Expr) (r : Lean.Level) (rOffset : Nat) :

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} [inst : ] [inst : ] (views : ) (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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.