This maps
n3 ↦ (dubious, n4)↦ (dubious, n4)
wheren3
is the lean 3 name andn4
is the corresponding lean 4 name.dubious
is either empty, or a warning message to be displayed whenn3
is translated, which indicates that the translation fromn3
ton4
is approximate and may cause downstream errors.toLean4 : Lean.NameMap (String × Lean.Name)This maps
n4 ↦ (n3, clashes)↦ (n3, clashes)
wheren4
is the lean 4 name andn3::clashes
is the list of all (non-synthetic
) declarations that map ton4
. (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
Equations
- Mathlib.Prelude.Rename.instInhabitedRenameMap = { default := { toLean4 := default, toLean3 := default } }
The lean 3 name.
n3 : Lean.NameThe lean 4 name, or
.anonymous
for a#noalign
.n4 : Lean.NameIf 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 : BoolA 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
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.
- 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
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.
Checks that id
has not already been #align
ed or #noalign
ed.
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.