Documentation

Mathlib.Mathport.Rename

source
ink
structure Mathlib.Prelude.Rename.RenameMap :
Type

  • This maps n3 ↦ (dubious, n4)↦ (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.

    toLean4 : Lean.NameMap (String × Lean.Name)

  • This maps n4 ↦ (n3, clashes)↦ (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.)

    toLean3 : Lean.NameMap (Lean.Name × List Lean.Name)

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

Instances For
    source
    ink
    instance Mathlib.Prelude.Rename.instInhabitedRenameMap :
    Inhabited Mathlib.Prelude.Rename.RenameMap
    Equations
    source
    ink
    structure Mathlib.Prelude.Rename.NameEntry :
    Type

    • The lean 3 name.

      n3 : Lean.Name

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

      n4 : Lean.Name

    • 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.

      synthetic : Bool

    • 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.

      dubious : String

    An olean entry for the rename extension.

    Instances For
      source
      ink
      def Mathlib.Prelude.Rename.RenameMap.insert (m : Mathlib.Prelude.Rename.RenameMap) (e : Mathlib.Prelude.Rename.NameEntry) :
      Mathlib.Prelude.Rename.RenameMap

      Insert a name entry into the RenameMap.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      def Mathlib.Prelude.Rename.RenameMap.find? (m : Mathlib.Prelude.Rename.RenameMap) :
      Lean.Name → Option (String × Lean.Name)

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

      Equations
      source
      ink
      opaque Mathlib.Prelude.Rename.renameExtension :
      Lean.SimplePersistentEnvExtension Mathlib.Prelude.Rename.NameEntry Mathlib.Prelude.Rename.RenameMap
      source
      ink
      def Mathlib.Prelude.Rename.getRenameMap (env : Lean.Environment) :
      Mathlib.Prelude.Rename.RenameMap
      Equations
      source
      ink
      def Mathlib.Prelude.Rename.addNameAlignment (n3 : Lean.Name) (n4 : Lean.Name) (synthetic : optParam Bool false) (dubious : optParam String "") :
      Lean.CoreM Unit
      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      opaque Mathlib.Prelude.Rename.binportTag :
      Lean.TagAttribute

      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).

      source
      ink
      def Mathlib.Prelude.Rename.removeX :
      Lean.Name → Lean.Name

      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
      source
      ink
      opaque Mathlib.Prelude.Rename.linter.uppercaseLean3 :
      Lean.Option Bool

      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.

      source
      ink
      opaque Mathlib.Prelude.Rename.align.precheck :
      Lean.Option Bool

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

      source
      ink
      def Mathlib.Prelude.Rename.align :
      Lean.ParserDescr

      #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.
      source
      ink
      def Mathlib.Prelude.Rename.ensureUnused {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (id : Lean.Name) :
      m Unit

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      def Mathlib.Prelude.Rename.suspiciousLean3Name (s : String) :
      Bool

      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.
      source
      ink
      def Mathlib.Prelude.Rename.elabAlign :
      Lean.Elab.Command.CommandElab

      Elaborate an #align command.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      def Mathlib.Prelude.Rename.noalign :
      Lean.ParserDescr

      #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.
      source
      ink
      def Mathlib.Prelude.Rename.elabNoAlign :
      Lean.Elab.Command.CommandElab

      Elaborate a #noalign command.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      def Mathlib.Prelude.Rename.lookup3 :
      Lean.ParserDescr

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

      Equations
      • One or more equations did not get rendered due to their size.
      source
      ink
      def Mathlib.Prelude.Rename.elabLookup3 :
      Lean.Elab.Command.CommandElab

      Elaborate a #lookup3 command.

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