Skip to main content

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.

Lean 4’s parser is fully extensible. You can introduce new syntax rules at any point in a file and immediately use them in subsequent code. The syntax command defines the grammar, while macro_rules or elab/elab_rules give it meaning. This page covers the full surface of Lean 4’s syntax extension API.

​
The syntax Command

The syntax command declares a new grammar rule without assigning semantics. It registers a parser for a syntax category (term, tactic, command, doElem, or a user-defined category). 
-- Basic form:
-- syntax <pattern> : <category>

-- A new term syntax
syntax "myBool" : term

-- A new tactic
syntax "solve_magic" : tactic

-- A new command
syntax "#list_defs" : command
Once declared, any occurrence of the specified pattern in source code is parsed into a Syntax node with a fresh syntax node kind (derived from the current namespace and name).

​
Parser Combinators

The grammar pattern in syntax is built from combinators. The most important ones are:
CombinatorMeaning
identAn identifier
numA numeric literal
strA string literal
termAny term
tacticAny tactic
"keyword"A literal token
p,*Zero or more p comma-separated
p,+One or more p comma-separated
p*Zero or more p
p+One or more p
p?Optional p
(p)Grouping
p \<|\> qOrdered choice
sepBy(p, sep)General separated list
ppSpacePretty-printer space hint
colGtIndentation: column greater than enclosing
-- A syntax accepting a list of identifiers
syntax "myVars" ident,+ : term

-- Optional clause
syntax "describe" ident ("as" str)? : command

-- Repeated terms
syntax "block" "{" term* "}" : term

-- Numeric or identifier argument
syntax "myOp" (num <|> ident) : term

​
Syntax Categories

Lean uses several built-in syntax categories:
CategoryUsed for
termExpressions
tacticTactics inside by blocks
commandTop-level declarations
doElemStatements inside do blocks
attrAttribute syntax (inside @[…])
stxRaw syntax fragments
You can define new categories with declare_syntax_cat: 
declare_syntax_cat myLang

syntax myLang : term  -- allow myLang fragments inside terms
syntax myLangExpr := myLang  -- give the category a parser alias

​
Syntax Priority

When multiple syntax rules could parse the same input, Lean uses priority to choose. Higher priority wins. The default priority is default (1000). 
-- Override with higher priority to shadow an existing rule
syntax (priority := high) "if" term "then" term : term

-- Explicit numeric priority
syntax (priority := 2000) mySpecialForm : tactic
High-priority syntax can shadow built-in rules. Use priorities carefully and prefer namespaced names to avoid conflicts.

​
elab: Inline Elaborator

The elab command combines syntax declaration and elaborator in a single step, analogously to how macro combines syntax + macro_rules: 
import Lean

open Lean Elab Term in
-- elab <pattern> : <category> => <elaboratorBody : TermElabM Expr>
elab "myNat" n:num : term => do
  let v := n.getNat
  return mkNatLit v

#eval myNat 42  -- 42
For tactic syntax: 
open Lean Elab Tactic in
elab "trace_goal" : tactic => do
  let goal ← getMainGoal
  let goalType ← goal.getType
  logInfo m!"Current goal type: {goalType}"
For commands: 
open Lean Elab Command in
elab "#list_constants" : command => do
  let env ← getEnv
  let consts := env.constants.toList.map (·.1)
  logInfo m!"Declared constants: {consts}"

​
elab_rules: Pattern-Matching Elaborator

elab_rules is the elaboration counterpart to macro_rules. It pattern-matches on the expanded syntax: 
open Lean Elab Term in
elab_rules : term
  | `(myPair $a $b) => do
    let ta ← elabTerm a none
    let tb ← elabTerm b none
    return mkApp2 (mkConst ``Prod.mk) ta tb

-- Multiple alternatives
elab_rules : term
  | `(myLit true)  => return mkConst ``Bool.true
  | `(myLit false) => return mkConst ``Bool.false

​
syntax + macro_rules vs syntax + elab

Use this when the meaning of your construct can be expressed entirely in terms of existing Lean syntax. The macro runs before elaboration; no type information is available.
syntax "myUnless" term "do" doSeq : doElem

macro_rules
  | `(doElem| myUnless $cond do $body) =>
    `(doElem| if !$cond then do $body)
Use this when you need access to types, the environment, or you need to produce Expr directly. Elaborators run in TermElabM and have the full meta-programming API.
syntax "typeOf" term : term

open Lean Elab Term in
elab_rules : term
  | `(typeOf $e) => do
    let e ← elabTerm e none
    inferType e

​
Complete Example: A Custom assert Command

This example defines an assert command that type-checks an expression against True or False at compile time and logs the result: 
import Lean
open Lean Elab Command Term Meta

-- Declare the syntax
syntax (name := assertCmd) "#assert" term : command

-- Attach the elaborator
@[command_elab assertCmd]
def elabAssertCmd : CommandElab
  | `(#assert $e) => do
      let val ← liftTermElabM <| do
        let e ← elabTerm e (some (mkConst ``Bool))
        let e ← whnf e
        return e
      match val with
      | .const ``Bool.true  _ => logInfo "Assertion passed: true"
      | .const ``Bool.false _ => logWarning "Assertion failed: false"
      | other => throwError "Expected a Bool literal, got: {other}"
  | _ => throwUnsupportedSyntax

-- Usage
#assert true    -- Assertion passed: true
#assert false   -- Assertion failed: false
#assert (1 == 1)  -- Assertion passed: true

​
Naming Syntax Nodes

By default, the syntax kind is derived automatically from the namespace. You can assign an explicit name with (name := myName): 
-- Explicit name for cross-module referencing
syntax (name := myModuleDebug) "#debug" ident : command

-- Reference the kind from macro_rules
macro_rules
  | `(command| #debug $id) => `(#check $id)
This is useful when you want to register an elaborator with @[command_elab myModuleDebug] from a different file.

​
Syntax in do Notation

Extending doElem lets you add new statements to do blocks: 
-- A "log then execute" do-element
syntax "logged" doElem : doElem

macro_rules
  | `(doElem| logged $e) => `(doElem| do
      IO.println "executing step"
      $e)

-- Usage
def run : IO Unit := do
  logged IO.println "hello"
  logged IO.println "world"

Build docs developers (and LLMs) love

Get started for freeTalk to us