Documentation

Lean.Elab.DefView

Instances For
    Equations
      Instances For
        Equations
          Instances For

            Header elaboration data of a DefView.

            • shortDeclName : Name

              Short name. Recall that all declarations in Lean 4 are potentially recursive. We use shortDeclName to refer to them at valueStx, and other declarations in the same mutual block.

            • declName : Name

              Full name for this declaration. This is the name that will be added to the Environment.

            • levelNames : List Name

              Universe level parameter names explicitly provided by the user.

            • binderIds : Array Syntax

              Syntax objects for the binders occurring before :, we use them to populate the InfoTree when elaborating valueStx.

            • numParams : Nat

              Number of parameters before :, it also includes auto-implicit parameters automatically added by Lean.

            • type : Expr

              Type including parameters.

            Instances For

              Snapshot after processing of a definition body.

              Instances For

                Snapshot after elaboration of a definition header.

                Instances For

                  State before elaboration of a mutual definition.

                  • fullHeaderRef : Syntax

                    Unstructured syntax object comprising the full "header" of the definition from the modifiers (incl. docstring) up to the value, used for determining header elaboration reuse.

                  • Elaboration result, unless fatal exception occurred.

                  Instances For

                    Snapshot after syntax tree has been split into separate mutual def headers.

                    Instances For
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    Equations
                                      Instances For
                                        Equations
                                          Instances For
                                            Equations
                                              Instances For
                                                Equations
                                                  Instances For
                                                    Equations
                                                      Instances For
                                                        Equations
                                                          Instances For