This structure keeps track of alignments from lean 3 names to lean 4 names and vice versa.
- n3 : Lean.Name
The lean 3 name.
- n4 : Lean.Name
The lean 4 name, or
- 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
n3is encountered by synport.
olean entry for the rename extension.
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.
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
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.
#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
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.
#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
- mod4 : Lean.Name
This is the same as
(← getEnv).header.mainModule, but we need access to it in
exportEntriesFnwhere the environment is not available.
The original list of import entries from imported files. We do not process these because only mathport actually uses it.
The import entries from the current file.
The data for
#align_import that is stored in memory while processing a lean file.