structure Mathlib.Prelude.Rename.RenameMap : Type

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

  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.

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

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

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

instance Mathlib.Prelude.Rename.instInhabitedRenameMap : Inhabited Mathlib.Prelude.Rename.RenameMap

structure Mathlib.Prelude.Rename.NameEntry : Type

• n3 : Lean.Name

  The lean 3 name.

• n4 : Lean.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.

An olean entry for the rename extension.

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.

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.

opaque Mathlib.Prelude.Rename.renameExtension : Lean.SimplePersistentEnvExtension Mathlib.Prelude.Rename.NameEntry Mathlib.Prelude.Rename.RenameMap

This extension stores the lookup data generated from #align commands.

def Mathlib.Prelude.Rename.addNameAlignment (n3 : Lean.Name) (n4 : Lean.Name) (synthetic : optParam Bool false) (dubious : optParam String "") : Lean.CoreM Unit

Insert a new name alignment into the rename extension.

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

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

• One or more equations did not get rendered due to their size.
• Mathlib.Prelude.Rename.removeX Lean.Name.anonymous = Lean.Name.anonymous
• Mathlib.Prelude.Rename.removeX (Lean.Name.num p n) = Lean.Name.num (Mathlib.Prelude.Rename.removeX p) n

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.

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

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

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.

def Mathlib.Prelude.Rename.ensureUnused {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (id : Lean.Name) : m Unit

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

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.

def Mathlib.Prelude.Rename.elabAlign : Lean.Elab.Command.CommandElab

Elaborate an #align command.

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.

def Mathlib.Prelude.Rename.elabNoAlign : Lean.Elab.Command.CommandElab

Elaborate a #noalign command.

def Mathlib.Prelude.Rename.lookup3 : Lean.ParserDescr

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

def Mathlib.Prelude.Rename.elabLookup3 : Lean.Elab.Command.CommandElab

Elaborate a #lookup3 command.

structure Mathlib.Prelude.Rename.ImportEntry : Type

• mod3 : Lean.Name

  The lean 3 name of the module.

• origin : Option (String × String)

  The original repository from which this module was derived.

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

structure Mathlib.Prelude.Rename.ImportState : Type

• mod4 : Lean.Name

  This is the same as (← getEnv).header.mainModule, but we need access to it in exportEntriesFn where the environment is not available.

• extern : Array (Array (Lean.Name × Mathlib.Prelude.Rename.ImportEntry))

  The original list of import entries from imported files. We do not process these because only mathport actually uses it.

• entries : List Mathlib.Prelude.Rename.ImportEntry

  The import entries from the current file.

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

instance Mathlib.Prelude.Rename.instInhabitedImportState : Inhabited Mathlib.Prelude.Rename.ImportState

opaque Mathlib.Prelude.Rename.renameImportExtension : Lean.PersistentEnvExtension (Lean.Name × Mathlib.Prelude.Rename.ImportEntry) (Lean.Name × Mathlib.Prelude.Rename.ImportEntry) Mathlib.Prelude.Rename.ImportState

This extension stores the lookup data generated from #align_import commands.

def Mathlib.Prelude.Rename.alignImport : Lean.ParserDescr

Declare the corresponding mathlib3 module for the current mathlib4 module.

def Mathlib.Prelude.Rename.elabAlignImport : Lean.Elab.Command.CommandElab

Elaborate a #align_import command.