structure Mathlib.Prelude.Rename.RenameMap : Type

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

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

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

Equations

• Mathlib.Prelude.Rename.instInhabitedRenameMap = { default := { toLean4 := default, toLean3 := default } }

structure Mathlib.Prelude.Rename.NameEntry : Type

An olean entry for the rename extension.

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

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.

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

• Mathlib.Prelude.Rename.RenameMap.find? m = Lean.NameMap.find? m.toLean4

instance Mathlib.Prelude.Rename.instInhabitedThunk {α : Type u_1} [Inhabited α] : Inhabited (Thunk α)

Equations

• Mathlib.Prelude.Rename.instInhabitedThunk = { default := Thunk.pure default }

opaque Mathlib.Prelude.Rename.renameExtension : Lean.SimplePersistentEnvExtension Mathlib.Prelude.Rename.NameEntry (Thunk 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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

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.

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.

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.

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.

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.

structure Mathlib.Prelude.Rename.ImportEntry : Type

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

• mod3 : Lean.Name

  The lean 3 name of the module.

• origin : Option (String × String)

  The original repository from which this module was derived.

structure Mathlib.Prelude.Rename.ImportState : Type

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

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

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

Equations

• Mathlib.Prelude.Rename.instInhabitedImportState = { default := { mod4 := default, extern := default, entries := default } }

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.

Equations

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

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

Elaborate a #align_import command.

Equations

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