Documentation

Lean.Elab.MutualInductive

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

For mutual ... end in particular:

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

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

  • ref : Syntax

    Syntax for the whole constructor.

  • modifiers : Modifiers
  • declName : Name

    Fully qualified name of the constructor.

  • declId : Syntax

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

  • binders : Syntax

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

  • type? : Option Syntax

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

Instances For
    Instances For

      A view for generic inductive types.

      Instances For

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

        Instances For

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

          Instances For

            An intermediate step for mutual inductive elaboration. See InductiveElabDescr

            • finalize : 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. The levelParams, params, and replaceIndFVars arguments of prefinalize are still valid here.

            Instances For

              An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

              Instances For

                An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

                Instances For

                  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 InductiveStep3.finalize.
                  Instances For

                    Environment extension to register inductive type elaborator commands.

                    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
                      Instances For

                        Initializes the elaborator associated to the given syntax.

                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For

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

                                    Equations
                                      Instances For

                                        Returns some ?m if u is of the form ?m + k. Returns none if u does not contain universe metavariables. Throw exception otherwise.

                                        Equations
                                          Instances For

                                            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.

                                            Equations
                                              Instances For

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

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

                                                    Executes k using the Syntax reference associated with constructor ctorName.

                                                    Equations
                                                      Instances For
                                                        def Lean.Elab.Command.InductiveView.withTypeRef {m : TypeType} {α : Type} [Monad m] [MonadRef m] (view : 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
                                                          Instances For
                                                            def Lean.Elab.Command.withViewTypeRef {m : TypeType} {α : Type} [Monad m] [MonadRef m] (views : Array InductiveView) (k : m α) :
                                                            m α
                                                            Equations
                                                              Instances For
                                                                Equations
                                                                  Instances For

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

                                                                    Equations
                                                                      Instances For

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

                                                                        Equations
                                                                          Instances For