# Documentation

Mathlib.Mathport.Rename

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

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

Instances For
Equations
• The lean 3 name.

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

• 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

Insert a name entry into the RenameMap.

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

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

Equations
def Mathlib.Prelude.Rename.addNameAlignment (n3 : Lean.Name) (n4 : Lean.Name) (synthetic : ) (dubious : ) :
Equations
• One or more equations did not get rendered due to their size.

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
• One or more equations did not get rendered due to their size.

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.
def Mathlib.Prelude.Rename.ensureUnused {m : } [inst : ] [inst : ] [inst : ] (id : Lean.Name) :

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

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

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.

Elaborate an #align command.

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

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

Elaborate a #noalign command.

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

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

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

Elaborate a #lookup3 command.

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