Lean.Elab.DeclModifiers

source

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

m Unit

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.

source

instance Lean.Elab.instInhabitedVisibility:

Inhabited Lean.Elab.Visibility

Equations

Lean.Elab.instInhabitedVisibility = { default := Lean.Elab.Visibility.regular }

source

instance Lean.Elab.instToStringVisibility:

ToString Lean.Elab.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.

source

instance Lean.Elab.instInhabitedRecKind:

Inhabited Lean.Elab.RecKind

Equations

Lean.Elab.instInhabitedRecKind = { default := Lean.Elab.RecKind.partial }

source

structure Lean.Elab.Modifiers:

Type

docString? : Option String
visibility : Lean.Elab.Visibility
isNoncomputable : Bool
recKind : Lean.Elab.RecKind
isUnsafe : Bool
attrs : Array Lean.Elab.Attribute

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

source

instance Lean.Elab.instInhabitedModifiers:

Inhabited Lean.Elab.Modifiers

Equations

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

source

def Lean.Elab.Modifiers.isPrivate:

Lean.Elab.Modifiers → Bool

Equations

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

source

def Lean.Elab.Modifiers.isProtected:

Lean.Elab.Modifiers → Bool

Equations

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

source

def Lean.Elab.Modifiers.isPartial:

Lean.Elab.Modifiers → Bool

Equations

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

source

def Lean.Elab.Modifiers.isNonrec:

Lean.Elab.Modifiers → Bool

Equations

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

source

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

Lean.Elab.Modifiers

Equations

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

source

instance Lean.Elab.instToFormatModifiers:

Lean.ToFormat Lean.Elab.Modifiers

Equations

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

source

instance Lean.Elab.instToStringModifiers:

ToString Lean.Elab.Modifiers

Equations

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

source

def Lean.Elab.expandOptDocComment? {m : Type → Type} [inst : Monad m] [inst : Lean.MonadError m] (optDocComment : Lean.Syntax) :

m (Option String)

Equations

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

source

def Lean.Elab.elabModifiers {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] (stx : Lean.Syntax) :

m Lean.Elab.Modifiers

Equations

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

source

def Lean.Elab.applyVisibility {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (visibility : Lean.Elab.Visibility) (declName : Lean.Name) :

m Lean.Name

Equations

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

source

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

m Unit

Equations

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

source

def Lean.Elab.mkDeclName {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (currNamespace : Lean.Name) (modifiers : Lean.Elab.Modifiers) (shortName : Lean.Name) :

m (Lean.Name × Lean.Name)

Equations

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

source

def Lean.Elab.expandDeclIdCore (declId : Lean.Syntax) :

Lean.Name × Lean.Syntax

Equations

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

source

structure Lean.Elab.ExpandDeclIdResult:

Type

shortName : Lean.Name
declName : Lean.Name
levelNames : List Lean.Name

source

def Lean.Elab.expandDeclId {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (currNamespace : Lean.Name) (currLevelNames : List Lean.Name) (declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) :

m Lean.Elab.ExpandDeclIdResult

Equations

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