Documentation Index
Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt
Use this file to discover all available pages before exploring further.
Attributes and linters are the tools Lean 4 uses to annotate declarations and enforce code-quality rules. Attributes fire during or after type-checking; linters scan syntax trees after each command. Both run in CoreM (via AttrM) and have full access to the environment.
The AttributeImpl Structure
Every attribute is backed by an AttributeImpl record defined in Lean.Attributes:
-- From Lean.Attributes
structure AttributeImpl extends AttributeImplCore where
/-- Called when the attribute is applied to declaration `decl`. -/
add (decl : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Unit
/-- Called when the attribute is removed. -/
erase (decl : Name) : AttrM Unit :=
throwError "Attribute `[{name}]` cannot be erased"
structure AttributeImplCore where
ref : Name := by exact decl_name% -- for go-to-definition
name : Name
descr : String
applicationTime := AttributeApplicationTime.afterTypeChecking
AttrM is an alias for CoreM, so attribute handlers can read the environment, throw errors, and log messages, but they cannot elaborate new terms.
AttributeApplicationTime
Controls when the add handler fires relative to the compilation pipeline:
inductive AttributeApplicationTime where
-- Default: fires after the kernel has type-checked the declaration.
| afterTypeChecking
-- Fires after the compiler has produced IR/native code.
| afterCompilation
-- Fires before elaboration of the declaration body starts.
| beforeElaboration
| Value | Use case |
|---|
afterTypeChecking | Register lemmas for simp, tag declarations, inspect types |
afterCompilation | Access compiled code info, @[extern]-style annotations |
beforeElaboration | Modify the elaboration environment before the body is processed |
AttributeKind
inductive AttributeKind
| global -- always active (default)
| local -- active only until current section/namespace/file ends
| scoped -- active only while the namespace is open
throwAttrMustBeGlobal if your attribute doesn’t support local or scoped:
if kind != .global then
throwAttrMustBeGlobal attr.name kind
registerBuiltinAttribute vs User Attributes
registerBuiltinAttribute
Used in builtin_initialize blocks (during interpreter startup) to register attributes that are part of the Lean core or a plugin:
builtin_initialize myAttr : TagAttribute ←
registerTagAttribute `myTag "marks declarations for special handling"
registerBuiltinAttribute can only be called during initialization (initializing returns true). Calling it later raises an error.
User-Defined Attributes
For attributes defined in normal Lean files (not core), use registerAttributeOfBuilder or, more commonly, the initialize block with registerBuiltinAttribute inside a plugin. Within a file, you can attach an AttributeImpl to the environment via Attribute.add.
In practice, most user code uses the higher-level helpers: TagAttribute, ParametricAttribute, or KeyedDeclsAttribute.
TagAttribute is the lightest-weight attribute. It simply records whether a declaration has been tagged; no parameters. Lookup is O(log n).
-- Register during initialization
builtin_initialize myTagAttr : TagAttribute ←
registerTagAttribute
`myTag
"A simple boolean tag attribute"
(validate := fun _decl => pure ()) -- optional validation
-- Query at any time
def isTagged (env : Environment) (decl : Name) : Bool :=
myTagAttr.hasTag env decl
-- Set the tag on a declaration
-- (Usually done automatically by the attribute handler)
-- myTagAttr.setTag env decl -- returns ExceptT
@[myTag] def myFunction : Nat := 42
ParametricAttribute — Attributes with Parameters
ParametricAttribute α attaches a value of type α to each tagged declaration:
-- Define what "getting the parameter" means
def myParamAttrImpl : ParametricAttributeImpl Nat where
name := `myParam
descr := "Attaches a natural number annotation to a declaration"
getParam decl stx := do
-- stx is the attribute syntax: @[myParam 42]
-- parse the numeric argument
if stx.getKind == `Lean.Parser.Attr.simple then
match stx[1][0].isNatLit? with
| some n => return n
| none => throwError "@[myParam] requires a numeric argument"
else
throwError "@[myParam] unexpected syntax"
builtin_initialize myParamAttr : ParametricAttribute Nat ←
registerParametricAttribute myParamAttrImpl
-- Query
def getMyParam (env : Environment) (decl : Name) : Option Nat :=
myParamAttr.getParam? env decl
@[myParam 7] def someDecl : Bool := true
-- getMyParam env `someDecl = some 7
KeyedDeclsAttribute — Dispatch Tables
KeyedDeclsAttribute γ powers Lean’s elaboration dispatch tables. It maps SyntaxNodeKind keys to lists of γ values (elaborator functions). This is how @[term_elab], @[tactic], @[command_elab], and @[macro] work internally.
-- From Lean.Elab.Tactic.Basic:
-- tacticElabAttribute : KeyedDeclsAttribute Tactic
-- Registered by:
unsafe builtin_initialize tacticElabAttribute : KeyedDeclsAttribute Tactic ←
mkElabAttribute Tactic `builtin_tactic `tactic
`Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic"
@[tactic myTacticKind] def myTac : Tactic := …, Lean stores myTac under key myTacticKind in tacticElabAttribute. When the elaborator encounters syntax of that kind, it looks up all registered functions and tries them in priority order.
You can create your own dispatch table for plugin architectures:
-- Define the handler type
abbrev MyHandler := Expr → CoreM Unit
-- Create the attribute
unsafe def mkMyHandlerAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute MyHandler) :=
KeyedDeclsAttribute.init {
name := `myHandler
descr := "Register a handler for a syntax kind"
valueTypeName := `MyHandler
} ref
@[implemented_by mkMyHandlerAttributeUnsafe]
opaque mkMyHandlerAttribute (ref : Name) : IO (KeyedDeclsAttribute MyHandler)
builtin_initialize myHandlerAttr : KeyedDeclsAttribute MyHandler ←
mkMyHandlerAttribute decl_name%
Built-in Attributes Overview
Lean 4 ships with many built-in attributes:
| Attribute | Purpose |
|---|
@[simp] | Register a lemma as a simp rule |
@[ext] | Generate extensionality lemmas |
@[norm_cast] | Register cast normalization lemma |
@[inline] | Hint to the compiler to inline this definition |
@[inline_if_reduce] | Inline only when the body can be reduced |
@[extern "c_fn"] | Link to an external C function |
@[reducible] | Mark definition as reducible (unfolded by reducible transparency) |
@[semireducible] | Default reducibility |
@[irreducible] | Never unfold (except with unfold) |
@[instance] | Register a typeclass instance |
@[class] | Mark a structure as a typeclass |
@[macro myKind] | Register a Macro function for a syntax kind |
@[tactic myKind] | Register a Tactic function for a tactic kind |
@[term_elab myKind] | Register a TermElab function |
@[command_elab myKind] | Register a CommandElab function |
The Linter API
Linters are functions that inspect the fully-elaborated Syntax of each command and emit warnings. They live in Lean.Linter and run in CommandElabM.
The Linter Structure
From Lean.Elab.Command:
structure Linter where
run : Syntax → CommandElabM Unit
name : Name := by exact decl_name%
addLinter: Registering a Linter
-- From Lean.Elab.Command:
-- def addLinter (l : Linter) : IO Unit
builtin_initialize addLinter {
name := `myLinter
run := fun stx => do
-- inspect the command syntax here
pure ()
}
addLinter is exported at the top level: export Lean.Elab.Command (Linter addLinter).
Writing a Linter: Full Example
A linter that warns when a def has a name starting with an underscore outside of a private scope:
import Lean
open Lean Elab Command Linter
register_builtin_option linter.noLeadingUnderscore : Bool := {
defValue := true
descr := "warn when a public def name starts with an underscore"
}
def noLeadingUnderscoreLinter : Linter where
name := `noLeadingUnderscore
run := fun stx => do
unless getLinterValue linter.noLeadingUnderscore (← getLinterOptions) do
return
-- Match top-level def commands
let `(def $id:ident $_ := $_) := stx | return
let name := id.getId
if name.toString.startsWith "_" then
logLint linter.noLeadingUnderscore id
s!"Public definition name '{name}' starts with an underscore"
builtin_initialize addLinter noLeadingUnderscoreLinter
logLint: Emitting Linter Diagnostics
-- From Lean.Linter.Init
def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
(opt : Lean.Option Bool) (ref : Syntax) (msg : MessageData) : m Unit
logLint respects the option’s enabled/disabled state automatically — if the option is false, the message is suppressed.
getLinterOptions and getLinterValue
-- Get the current linter option set (environment + options combined)
def getLinterOptions [Monad m] [MonadOptions m] [MonadEnv m] : m LinterOptions
-- Check if a specific linter is enabled
def getLinterValue (opt : Lean.Option Bool) (o : LinterOptions) : Bool
Built-in Linters
Lean ships with these linters (all under linter.*):
| Option | Description |
|---|
linter.unusedVariables | Warn on unused function parameters |
linter.missingDocs | Warn on undocumented public declarations |
linter.deprecated | Warn on use of deprecated declarations |
linter.checkUnivs | Check for unused universe parameters |
linter.constructorNameAsVariable | Warn when constructor names shadow variable names |
linter.defProp | Warn about def used for propositions (suggest theorem) |
linter.ambiguousOpen | Warn on ambiguous open scopes |
linter.suspiciousUnexpanderPatterns | Warn on @[app_unexpander] matching literal names |
linter.unusedVariables.funArgs | Warn on unused explicit function arguments |
linter.all | Enable all linters at once |
linter.extra | Enable extra linters (off by default, used by lake lint) |
Disabling Linters
-- Disable for the rest of the file
set_option linter.unusedVariables false
-- Disable for a single declaration
@[nolint unusedVariables]
def myDef (x : Nat) : Nat := 0
-- Or with a region
section
set_option linter.missingDocs false
def undocumented := 42
end
Use set_option linter.all true in CI to enable every linter and catch issues early. Individual linters can then be disabled selectively where they produce false positives.
