Documentation

Lean.Elab.DeclModifiers

source
def Lean.Elab.checkNotAlreadyDeclared {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (declName : Name) :
m Unit

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
  • One or more equations did not get rendered due to their size.
source
inductive Lean.Elab.Visibility :
Type

Declaration visibility modifier. That is, whether a declaration is regular, protected or private.

Instances For
source
instance Lean.Elab.instInhabitedVisibility :
Inhabited Visibility
Equations
source
instance Lean.Elab.instToStringVisibility :
ToString Visibility
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.Elab.RecKind :
Type

Whether a declaration is default, partial or nonrec.

Instances For
source
instance Lean.Elab.instInhabitedRecKind :
Inhabited RecKind
Equations
source
structure Lean.Elab.Modifiers :
Type

Flags and data added to declarations (eg docstrings, attributes, private, unsafe, partial, ...).

Instances For
source
instance Lean.Elab.instInhabitedModifiers :
Inhabited Modifiers
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Modifiers.isPrivate :
Modifiers → Bool
Equations
  • One or more equations did not get rendered due to their size.
  • x✝.isPrivate = false
source
def Lean.Elab.Modifiers.isProtected :
Modifiers → Bool
Equations
  • One or more equations did not get rendered due to their size.
  • x✝.isProtected = false
source
def Lean.Elab.Modifiers.isPartial :
Modifiers → Bool
Equations
  • One or more equations did not get rendered due to their size.
  • x✝.isPartial = false
source
def Lean.Elab.Modifiers.isNonrec :
Modifiers → Bool
Equations
  • One or more equations did not get rendered due to their size.
  • x✝.isNonrec = false
source
def Lean.Elab.Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) :
Modifiers

Adds attribute attr in modifiers

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) :
Modifiers

Filters attributes using p

Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Elab.instToFormatModifiers :
ToFormat Modifiers
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Elab.instToStringModifiers :
ToString Modifiers
Equations
source
def Lean.Elab.expandOptDocComment? {m : Type → Type} [Monad m] [MonadError m] (optDocComment : Syntax) :
m (Option String)

Retrieve doc string from stx of the form (docComment)?.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.elabModifiers {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : TSyntax `Lean.Parser.Command.declModifiers) :
m Modifiers

Elaborate declaration modifiers (i.e., attributes, partial, private, protected, unsafe, noncomputable, doc string)

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.applyVisibility {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (visibility : Visibility) (declName : Name) :
m Name

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
source
def Lean.Elab.checkIfShadowingStructureField {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) :
m Unit
Equations
source
def Lean.Elab.mkDeclName {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) :
m (Name × Name)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.expandDeclIdCore (declId : Syntax) :
Name × Syntax

declId is of the form

leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")

but we also accept a single identifier to users to make macro writing more convenient .

Equations
source
structure Lean.Elab.ExpandDeclIdResult :
Type

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.

  • levelNames : List Name

    Universe parameter names provided using the universe command and .{...} notation.

source
def Lean.Elab.expandDeclId {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadInfoTree m] [MonadLiftT IO m] (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) :
m ExpandDeclIdResult

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.

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