Ensure the environment does not contain a declaration with name declName
.
Recall that a private declaration cannot shadow a non-private one and vice-versa, although
they internally have different names.
Equations
Instances For
Declaration visibility modifier. That is, whether a declaration is regular, protected or private.
- regular : Visibility
- protected : Visibility
- private : Visibility
Instances For
Flags and data added to declarations (eg docstrings, attributes, private
, unsafe
, partial
, ...).
- stx : TSyntax `Lean.Parser.Command.declModifiers
Input syntax, used for adjusting declaration range (unless missing)
- visibility : Visibility
- isNoncomputable : Bool
- recKind : RecKind
- isUnsafe : Bool
Instances For
Adds attribute attr
in modifiers
Equations
Instances For
Retrieve doc string from stx
of the form (docComment)?
.
Equations
Instances For
Elaborate declaration modifiers (i.e., attributes, partial
, private
, protected
, unsafe
, noncomputable
, doc string)
Equations
Instances For
Ensure the function has not already been declared, and apply the given visibility setting to declName
.
If private
, return the updated name using our internal encoding for private names.
If protected
, register declName
as protected in the environment.
Equations
Instances For
Equations
Instances For
Equations
Instances For
expandDeclId
resulting type.
- shortName : Name
Short name for recursively referring to the declaration.
- declName : Name
Fully qualified name that will be used to name the declaration in the kernel.
Universe parameter names provided using the
universe
command and.{...}
notation.
Instances For
Given a declaration identifier (e.g., ident (".{" ident,+ "}")?
) that may contain explicit universe parameters
- Ensure the new universe parameters do not shadow universe parameters declared using
universe
command. - Create the fully qualified named for the declaration using the current namespace, and given
modifiers
- Create a short version for recursively referring to the declaration. Recall that the
protected
modifier affects the generation of the short name.
The result also contains the universe parameters provided using universe
command, and the .{...}
notation.
This commands also stores the doc string stored in modifiers
.