Documentation

Mathlib.Mathport.Rename

This structure keeps track of alignments from lean 3 names to lean 4 names and vice versa.

  • This maps n3 ↦ (dubious, n4) where n3 is the lean 3 name and n4 is the corresponding lean 4 name. dubious is either empty, or a warning message to be displayed when n3 is translated, which indicates that the translation from n3 to n4 is approximate and may cause downstream errors.

  • This maps n4 ↦ (n3, clashes) where n4 is the lean 4 name and n3::clashes is the list of all (non-synthetic) declarations that map to n4. (That is, we do not assume the mapping from lean 3 to lean 4 name is injective.)

Instances For

    An olean entry for the rename extension.

    • The lean 3 name.

    • The lean 4 name, or .anonymous for a #noalign.

    • synthetic : Bool

      If true, this lean 3 -> lean 4 mapping will not be entered into the converse map. This is used for "internal" definitions that should never be referred to in the source syntax.

    • dubious : String

      A dubious translation is one where there is a type mismatch from the translated lean 3 definition to a pre-existing lean 4 definition. Type errors are likely in downstream theorems. The string stored here is printed in the event that n3 is encountered by synport.

    Instances For

      Insert a name entry into the RenameMap.

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

        Look up a lean 4 name from the lean 3 name. Also return the dubious error message.

        Equations
        • m.find? = m.toLean4.find?
        Instances For
          Equations
          • Mathlib.Prelude.Rename.instInhabitedThunk_mathlib = { default := Thunk.pure default }

          Insert a new name alignment into the rename extension.

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

            The @[binport] attribute should not be added manually, it is added automatically by mathport to definitions that it created based on a lean 3 definition (as opposed to pre-existing definitions).

            Removes all occurrences of from the name. This is the same processing used by mathport to generate name references, and declarations with are used to align declarations that do not defeq match the originals.

            Equations
            Instances For

              Because lean 3 uses a lowercase snake case convention, it is expected that all lean 3 declaration names should use lowercase, with a few rare exceptions for categories and the set union operator. This linter warns if you use uppercase in the lean 3 part of an #align statement, because this is most likely a typo. But if the declaration actually uses capitals it is not unusual to disable this lint locally or at file scope.

              Check that the referenced lean 4 definition exists in an #align directive.

              #align lean_3.def_name Lean4.defName will record an "alignment" from the lean 3 name to the corresponding lean 4 name. This information is used by the mathport utility to translate later uses of the definition.

              If there is no alignment for a given definition, mathport will attempt to convert from the lean 3 snake_case style to UpperCamelCase for namespaces and types and lowerCamelCase for definitions, and snake_case for theorems. But for various reasons, it may fail either to determine whether it is a type, definition, or theorem, or to determine that a specific definition is in fact being called. Or a specific definition may need a different name altogether because the existing name is already taken in lean 4 for something else. For these reasons, you should use #align on any theorem that needs to be renamed from the default.

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

                Checks that id has not already been #aligned or #noaligned.

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

                  Purported Lean 3 names containing capital letters are suspicious. However, we disregard capital letters occurring in a few common names.

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

                    Elaborate an #align command.

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

                      #noalign lean_3.def_name will record that lean_3.def_name has been marked for non-porting. This information is used by the mathport utility, which will remove the declaration from the corresponding mathport file, and later uses of the definition will be replaced by sorry.

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

                        Elaborate a #noalign command.

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

                          Show information about the alignment status of a lean 3 definition.

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

                            Elaborate a #lookup3 command.

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

                              An entry in the #align_import extension, containing all the data in the command.

                              Instances For

                                The data for #align_import that is stored in memory while processing a lean file.

                                Instances For
                                  Equations

                                  Declare the corresponding mathlib3 module for the current mathlib4 module.

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

                                    Elaborate a #align_import command.

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