Lean.Elab.Inductive

source

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.

source

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.

source

structure Lean.Elab.Command.CtorView:

Type

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

source

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 } }

source

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

source

instance Lean.Elab.Command.instInhabitedInductiveView:

Inhabited Lean.Elab.Command.InductiveView

Equations

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

source

structure Lean.Elab.Command.ElabHeaderResult:

Type

source

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 } }

source

def Lean.Elab.Command.shouldInferResultUniverse (u : Lean.Level) :

Lean.Elab.TermElabM (Option Lean.MVarId)

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.

source

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.

source

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

source

def Lean.Elab.Command.accLevel.go (r : Lean.Level) (u : Lean.Level) (rOffset : Nat) :

OptionT (StateT (Array Lean.Level) Id) Unit

source

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