opaque Lean.linter.redundantVisibility : Lean.Option Bool

def Lean.Elab.checkNotAlreadyDeclared {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadFinally 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.

inductive Lean.Elab.Visibility : Type

Declaration visibility modifier. That is, whether a declaration is public or private or inherits its visibility from the outer scope.

• regular : Visibility
• private : Visibility
• public : Visibility

@[implicit_reducible]

instance Lean.Elab.instInhabitedVisibility : Inhabited Visibility

Equations

• Lean.Elab.instInhabitedVisibility = { default := Lean.Elab.instInhabitedVisibility.default }

@[implicit_reducible]

instance Lean.Elab.instToStringVisibility : ToString Visibility

Equations

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

def Lean.Elab.Visibility.isPrivate : Visibility → Bool

Equations

• Lean.Elab.Visibility.private.isPrivate = true
• x✝.isPrivate = false

def Lean.Elab.Visibility.isPublic : Visibility → Bool

Equations

• Lean.Elab.Visibility.public.isPublic = true
• x✝.isPublic = false

def Lean.Elab.Visibility.isInferredPublic (env : Environment) (v : Visibility) : Bool

Returns whether the given visibility modifier should be interpreted as public in the current environment.

NOTE: Environment.isExporting defaults to false when command elaborators are invoked for backward compatibility. It needs to be initialized apropriately first before calling this function as e.g. done in elabDeclaration.

Equations

• Lean.Elab.Visibility.isInferredPublic env v = if (env.isExporting || !env.header.isModule) = true then !v.isPrivate else v.isPublic

def Lean.Elab.elabVisibility {m : Type → Type} [Monad m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (vis? : Option (TSyntax `Lean.Parser.Command.visibility)) : m Visibility

Converts optional visibility syntax to a Visibility value.

Equations

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

inductive Lean.Elab.RecKind : Type

Whether a declaration is default, partial or nonrec.

• partial : RecKind
• nonrec : RecKind
• default : RecKind

@[implicit_reducible]

instance Lean.Elab.instInhabitedRecKind : Inhabited RecKind

Equations

• Lean.Elab.instInhabitedRecKind = { default := Lean.Elab.instInhabitedRecKind.default }

inductive Lean.Elab.ComputeKind : Type

Codegen-relevant modifiers.

• regular : ComputeKind
• meta : ComputeKind
• noncomputable : ComputeKind

@[implicit_reducible]

instance Lean.Elab.instInhabitedComputeKind : Inhabited ComputeKind

Equations

• Lean.Elab.instInhabitedComputeKind = { default := Lean.Elab.instInhabitedComputeKind.default }

def Lean.Elab.instBEqComputeKind.beq : ComputeKind → ComputeKind → Bool

Equations

• Lean.Elab.instBEqComputeKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.Elab.instBEqComputeKind : BEq ComputeKind

Equations

• Lean.Elab.instBEqComputeKind = { beq := Lean.Elab.instBEqComputeKind.beq }

def Lean.Elab.instReprComputeKind.repr : ComputeKind → Nat → Format

Equations

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

@[implicit_reducible]

instance Lean.Elab.instReprComputeKind : Repr ComputeKind

Equations

• Lean.Elab.instReprComputeKind = { reprPrec := Lean.Elab.instReprComputeKind.repr }

structure Lean.Elab.Modifiers : Type

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)

• docString? : Option (TSyntax `Lean.Parser.Command.docComment × Bool)

  The docstring, if present, and whether it's Verso.

• visibility : Visibility
• isProtected : Bool
• computeKind : ComputeKind
• recKind : RecKind
• isUnsafe : Bool
• attrs : Array Attribute

@[implicit_reducible]

instance Lean.Elab.instInhabitedModifiers : Inhabited Modifiers

Equations

• Lean.Elab.instInhabitedModifiers = { default := Lean.Elab.instInhabitedModifiers.default }

def Lean.Elab.Modifiers.isPrivate (m : Modifiers) : Bool

Equations

• m.isPrivate = m.visibility.isPrivate

def Lean.Elab.Modifiers.isPublic (m : Modifiers) : Bool

Equations

• m.isPublic = m.visibility.isPublic

def Lean.Elab.Modifiers.isInferredPublic (env : Environment) (m : Modifiers) : Bool

Equations

• Lean.Elab.Modifiers.isInferredPublic env m = Lean.Elab.Visibility.isInferredPublic env m.visibility

def Lean.Elab.Modifiers.isPartial : Modifiers → Bool

Equations

• One or more equations did not get rendered due to their size.
• x✝.isPartial = false

def Lean.Elab.Modifiers.isNonrec : Modifiers → Bool

Equations

• One or more equations did not get rendered due to their size.
• x✝.isNonrec = false

def Lean.Elab.Modifiers.isMeta (m : Modifiers) : Bool

Equations

• m.isMeta = match m.computeKind with | Lean.Elab.ComputeKind.meta => true | x => false

def Lean.Elab.Modifiers.isNoncomputable (m : Modifiers) : Bool

Equations

• m.isNoncomputable = match m.computeKind with | Lean.Elab.ComputeKind.noncomputable => true | x => false

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.

def Lean.Elab.Modifiers.addFirstAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers

Adds attribute attr in modifiers, at the beginning

Equations

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

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.

def Lean.Elab.Modifiers.anyAttr (modifiers : Modifiers) (p : Attribute → Bool) : Bool

Returns true if modifiers contains an attribute satisfying p.

Equations

• modifiers.anyAttr p = modifiers.attrs.any p

@[implicit_reducible]

instance Lean.Elab.instToFormatModifiers : ToFormat Modifiers

Equations

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

@[implicit_reducible]

instance Lean.Elab.instToStringModifiers : ToString Modifiers

Equations

• Lean.Elab.instToStringModifiers = { toString := toString ∘ Std.format }

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.

def Lean.Elab.elabModifiers {m : Type → Type} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadFinally 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, meta, noncomputable, doc string)

Equations

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

def Lean.Elab.applyVisibility {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadFinally m] [MonadInfoTree m] (modifiers : Modifiers) (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

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.checkIfShadowingStructureField declName = pure ()

def Lean.Elab.mkDeclName {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] [MonadFinally 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.

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

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

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.

• docString? : Option (TSyntax `Lean.Parser.Command.docComment × Bool)

  The docstring, and whether it's Verso

def Lean.Elab.expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) : TermElabM 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.

@[inline]

def Lean.Elab.Term.withDeprecationContextFromAttrs {m : Type → Type u_1} {α : Type} [MonadWithReaderOf Context m] (attrs : Array Attribute) : m α → m α

If attrs contains an @[deprecated] attribute, runs the action with Term.Context.checkDeprecated disabled, suppressing the linter.deprecated warning that would otherwise fire when a deprecated constant is referenced. Otherwise, runs the action unchanged.

This implements the suppression rule from RFC #8942: deprecation warnings should not fire inside the body of a declaration that is itself marked @[deprecated], since the references will go away along with the declaration.

Equations

• Lean.Elab.Term.withDeprecationContextFromAttrs attrs = if (attrs.any fun (x : Lean.Elab.Attribute) => x.name == `deprecated) = true then Lean.Elab.Term.withoutCheckDeprecated else id