Elaborator framework for (mutual) inductives

This module defines the framework for elaborating (mutually recursive) inductive types. Commands such as inductive and structure plug into this framework, and the framework orchestrates their mutual elaboration.

The main entry point for new inductive commands are the @[builtin_inductive_elab]/@[inductive_elab] attributes, which register a handler for a given decl syntax.

The main entry point to elaboration are the functions

• Lean.Elab.Command.isInductiveCommand to determine whether syntax has a registered inductive elaborator.
• Lean.Elab.Command.elabInductives to elaborate a list of syntaxes as mutually inductive types.
• Lean.Elab.Command.elabInductive to elaborate a single inductive command.

For mutual ... end in particular:

• Lean.Elab.Command.isMutualInductive to check whether each syntax element of a mutual ... end block has a registered inductive elaborator.
• Lean.Elab.Command.elabMutualInductive to elaborate a list of syntaxes satisfying isMutualInductive as a mutually inductive block.

See the docstring on Lean.Elab.Command.InductiveElabDescr for an overview of the framework.

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

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

structure Lean.Elab.Command.CtorView : Type

View of a constructor. Only ref, modifiers, declName, and declId are required by the mutual inductive elaborator itself.

• ref : Lean.Syntax

  Syntax for the whole constructor.

• modifiers : Lean.Elab.Modifiers
• declName : Lean.Name

  Fully qualified name of the constructor.

• declId : Lean.Syntax

  Syntax for the name of the constructor, used to apply terminfo. If the source is synthetic, terminfo is not applied.

• binders : Lean.Syntax

  For handler use. The inductive uses it for the binders to the constructor.

• type? : Option Lean.Syntax

  For handler use. The inductive command uses it for the resulting type for the constructor.

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

Equations

• Lean.Elab.Command.instInhabitedCtorView = { default := { ref := default, modifiers := default, declName := default, declId := 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

A view for generic inductive types.

• ref : Lean.Syntax
• declId : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• isClass : Bool
• allowIndices : Bool

  Whether the command should allow indices (like inductive) or not (like structure).

• allowSortPolymorphism : Bool

  Whether the command supports creating inductive types that can be polymorphic across both Prop and Type _. If false, then either the universe must be Prop or it must be of the form Type _.

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

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.PreElabHeaderResult : Type

Elaborated header for an inductive type before fvars for each inductive are added to the local context.

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

instance Lean.Elab.Command.instInhabitedPreElabHeaderResult : Inhabited Lean.Elab.Command.PreElabHeaderResult

structure Lean.Elab.Command.ElabHeaderResultextends Lean.Elab.Command.PreElabHeaderResult : Type

The elaborated header with the indFVar registered for this inductive type.

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

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

Equations

• Lean.Elab.Command.instInhabitedElabHeaderResult = { default := { toPreElabHeaderResult := default, indFVar := default } }

structure Lean.Elab.Command.InductiveElabStep2 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

• ctors : List Lean.Constructor

  The constructors produced by InductiveElabStep1.

• collectUsedFVars : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit

  Function to collect additional fvars that might be missed by the constructors. It is permissible to include fvars that do not exist in the local context (structure for example includes its field fvars).

• checkUniverses : Nat → Lean.Level → Lean.Elab.TermElabM Unit

  Function to check universes and provide a custom error. (structure uses this to do checks per field to give nicer messages.)

• finalizeTermElab : Lean.Elab.TermElabM Unit

  Step to finalize term elaboration, done immediately after universe level processing is complete.

• prefinalize : List Lean.Name → Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Unit

  Like finalize, but occurs before afterTypeChecking attributes.

• finalize : List Lean.Name → Array Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Unit

  Finalize the inductive type, after they are all added to the environment, after auxiliary definitions are added, and after computed fields are registered.

instance Lean.Elab.Command.instInhabitedInductiveElabStep2 : Inhabited Lean.Elab.Command.InductiveElabStep2

structure Lean.Elab.Command.InductiveElabStep1 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

• view : Lean.Elab.Command.InductiveView
• elabCtors : Array Lean.Elab.Command.ElabHeaderResult → Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2

instance Lean.Elab.Command.instInhabitedInductiveElabStep1 : Inhabited Lean.Elab.Command.InductiveElabStep1

structure Lean.Elab.Command.InductiveElabDescr : Type

Descriptor for a command processor that elaborates an inductive type.

Elaboration occurs in the following steps:

• Every command has its mkInductiveView evaluated, producing InductiveViews and callbacks for the next steps (all recorded in InductiveElabStep1).
• Each InductiveView gets elaborated, creating ElabHeaderResults, and the local contexts are unified into a single one with a consistent set of parameters between each inductive.
• Each callback is called to elaborate each inductives' constructors and some additional callbacks (all recorded in InductiveElabStep2).
• Fvars are collected from the constructors and from the InductiveStep2.collectUsedFVars callbacks. This is used to compute the final set of scoped variables that should be used as additional parameters.
• Universe levels are checked. Commands can give custom errors using InductiveStep2.collectUniverses.
• Elaboration of constructors is finalized, with additional tasks done by each InductiveStep2.collectUniverses.
• The inductive family is added to the environment and is checked by the kernel.
• Attributes and other finalization activities are performed, including those defined by InductiveStep2.prefinalize and InductiveStep2.finalize.

• mkInductiveView : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1

instance Lean.Elab.Command.instInhabitedInductiveElabDescr : Inhabited Lean.Elab.Command.InductiveElabDescr

opaque Lean.Elab.Command.inductiveElabAttr : Lean.KeyedDeclsAttribute Lean.Elab.Command.InductiveElabDescr

Environment extension to register inductive type elaborator commands.

def Lean.Elab.Command.isInductiveCommand {m : Type → Type} [Monad m] [Lean.MonadEnv m] (stx : Lean.Syntax) : m Bool

Returns true if the syntax partipates in the mutual inductive elaborator. These do not need to be commands. In fact inductive and structure are registered on the Lean.Parser.Command.inductive and Lean.Parser.Command.structure syntaxes.

Equations

• Lean.Elab.Command.isInductiveCommand stx = do let env ← Lean.getEnv pure !(Lean.Elab.Command.inductiveElabAttr.getEntries env stx.getKind).isEmpty

def Lean.Elab.Command.mkInductiveView (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep1

Initializes the elaborator associated to the given syntax.

Equations

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

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

def Lean.Elab.Command.withExplicitToImplicit {α : Type} (xs : Array Lean.Expr) (k : Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

Execute k with updated binder information for xs. Any x that is explicit becomes implicit.

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)

Returns some ?m if u is of the form ?m + k. Returns 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.accLevel (u r : Lean.Level) (rOffset : Nat) : ExceptT Lean.MessageData (StateT Lean.Elab.Command.AccLevelState✝ Id) Unit

Auxiliary function for updateResultingUniverse. Consider the constraint u ≤ ?r + rOffset where u has no metavariables except for perhaps ?r. This function attempts to find a unique minimal solution of the form ?r := max l₁ ... lₙ where each lᵢ is normalized and not a max/imax.

It also records information about how "too big" rOffset is. Consider u ≤ ?r + 1, from for example

inductive I (α : Sort u) : Type _ where
  | mk (x : α)

This is likely a mistake. The correct solution would be Type (max u 1) rather than Type (u + 1), but by this point it is impossible to rectify. So, for u ≤ ?r + 1 we record the pair of u and 1 so that we can inform the user what they should have probably used instead.

def Lean.Elab.Command.accLevel.go (r u : Lean.Level) (rOffset : Nat) : ExceptT Lean.MessageData (StateT Lean.Elab.Command.AccLevelState✝ Id) Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Command.accLevel.go r (u_2.max v) rOffset = do Lean.Elab.Command.accLevel.go r u_2 rOffset Lean.Elab.Command.accLevel.go r v rOffset
• Lean.Elab.Command.accLevel.go r (u_2.imax v) rOffset = do Lean.Elab.Command.accLevel.go r u_2 rOffset Lean.Elab.Command.accLevel.go r v rOffset
• Lean.Elab.Command.accLevel.go r Lean.Level.zero rOffset = pure ()
• Lean.Elab.Command.accLevel.go r u_2.succ rOffset_2.succ = Lean.Elab.Command.accLevel.go r u_2 rOffset_2

def Lean.Elab.Command.accLevelAtCtor (ctorParam : Lean.Expr) (r : Lean.Level) (rOffset : Nat) : StateT Lean.Elab.Command.AccLevelState✝ Lean.Elab.TermElabM Unit

Auxiliary function for updateResultingUniverse. Applies accLevel to the given constructor parameter.

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 α

Executes k using the Syntax reference associated with constructor ctorName.

def Lean.Elab.Command.InductiveView.withTypeRef {m : Type → Type} {α : Type} [Monad m] [Lean.MonadRef m] (view : Lean.Elab.Command.InductiveView) (k : m α) : m α

Runs k with the resulting type as the ref or, if that's not available, with the view's ref.

Equations

• view.withTypeRef k = Lean.withRef view.ref (match view.type? with | some type => Lean.withRef type k | none => k)

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

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

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

def Lean.Elab.Command.isMutualInductive {m : Type → Type} [Monad m] [Lean.MonadEnv m] (stx : Lean.Syntax) : m Bool

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

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

Elaborates a mutual block, assuming the commands satisfy Lean.Elab.Command.isMutualInductive.