21.6. Elaborators🔗

While macros allow Lean to be extended by translating new syntax into existing syntax, elaborators allow the new syntax to be processed directly. Elaborators have access to everything that Lean itself uses to implement each feature of the language. Defining a new elaborator allows a language extension to be just as powerful as any built-in feature of Lean.

Elaborators come in two varieties:

Command elaborators are used to add new commands to Lean. Commands are implemented as side effects: they may add new constants to the global environment, extend compile-time tables such as the one that tracks instances, they can provide feedback in the form of information, warnings, or errors, and they have full access to the IO monad. Command elaborators are associated with the syntax kinds that they can handle.
Term elaborators are used to implement new terms by translating the syntax into Lean's core type theory. They can do everything that command elaborators can do, and they additionally have access to the local context in which the term is being elaborated. Term elaborators can look up bound variables, bind new variables, unify two terms, and much more. A term elaborator must return a value of type Lean.Expr, which is the AST of the core type theory.

This section provides an overview and a few examples of elaborators. Because Lean's own elaborator uses the same tools, the source code of the elaborator is a good source of further examples. Just like macros, multiple elaborators may be associated with a syntax kind; they are tried in order, and elaborators may delegate to the next elaborator in the table by throwing the unsupportedSyntax exception.

syntaxElaboration Rules

The Lean.Parser.Command.elab_rules : commandelab_rules command takes a sequence of elaboration rules, specified as syntax pattern matches, and adds each as an elaborator. The rules are attempted in order, before previously-defined elaborators, and later elaborators may add further options.

command ::= ...
    | A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
`plainDocComment` to always treat the contents as plain text.

A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/`
in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node.
A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
docComment?
      (@[attrInstance,*])?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind elab_rules ((kind := ident))? (: ident)? (<= ident)?
        (| Syntax quotation for terms. `((p : identp:ident|)?Suitable syntax for p : identp ) => term)*

Commands, terms, and tactics each maintain a table that maps syntax kinds to elaborators. The syntax category for which the elaborator should be used is specified after the colon, and must be term, command, or tactic. The Lean.Parser.Command.elab_rules : command<= binds the provided identifier to the current expected type in the context in which a term is being elaborated; it may only be used for term elaborators, and if present, then term is implied as the syntax category.

attributeElaborator Attribute

Elaborators can be directly associated with syntax kinds by applying the appropriate attributes. Each takes the name of a syntax kind and associates the definition with the kind.

attr ::= ...
    | term_elab (prio
       | ident)

attr ::= ...
    | command_elab (prio
       | ident)

attr ::= ...
    | tactic (prio
       | ident)

21.6.1. Command Elaborators

A command elaborator has type CommandElab, which is an abbreviation for Syntax → CommandElabM Unit. Command elaborators may be implicitly defined using Lean.Parser.Command.elab_rules : commandelab_rules, or explicitly by defining a function and applying the command_elab attribute.

Querying the Environment

A command elaborator can be used to query the environment to discover how many constants have a given name. This example uses getEnv from the MonadEnv class to get the current environment. Environment.constants yields a mapping from names to information about them (e.g. their type and whether they are a definition, inductive type declaration, etc). logInfoAt allows informational output to be associated with syntax from the original program, and a token antiquotation is used to implement the Lean convention that output from interactive commands is associated with their keyword.

syntax "#count_constants " ident : command

elab_rules : command
  | `(#count_constants%$tok $x) => do
    let pattern := x.getId
    let env ← getEnv
    let mut count := 0
    for (y, _) in env.constants do
      if pattern.isSuffixOf y then
        count := count + 1
    logInfoAt tok m!"Found {count} instances of '{pattern}'"

def interestingName := 55
def NS.interestingName := "Another one"

Found 2 instances of 'interestingName'#count_constants interestingName

Found 2 instances of 'interestingName'

Live ↪

21.6.2. Term Elaborators

A term elaborator has type TermElab, which is an abbreviation for Syntax → Option Expr → TermElabM Expr. The optional Expr parameter is the type expected for the term being elaborated, which is none if no type is yet known. Like command elaborators, term elaborators may be implicitly defined using Lean.Parser.Command.elab_rules : commandelab_rules, or explicitly by defining a function and applying the term_elab attribute.

Avoiding a Type

This examples demonstrates an elaborator for syntax that is the opposite of a type ascription. The provided term may have any type other than the one indicated, and metavariables are solved pessimistically. In this example, elabType invokes the term elaborator and then ensures that the resulting term is a type. Meta.inferType infers a type for a term, and Meta.isDefEq attempts to make two terms definitionally equal by unification, returning true if it succeeds.

syntax (name := notType) "(" term  " !: " term ")" : term

@[term_elab notType]
def elabNotType : TermElab := fun stx _ => do
  let `(($tm:term !: $ty:term)) := stx
    | throwUnsupportedSyntax
  let unexpected ← elabType ty
  let e ← elabTerm tm none
  let eTy ← Meta.inferType e
  if (← Meta.isDefEq eTy unexpected) then
    throwErrorAt tm m!"Got unwanted type {eTy}"
  else pure e

If the type position does not contain a type, then elabType throws an error:

#eval ([1, 2, 3] !: type expected, got
  ("not a type" : String)"not a type")

type expected, got
  ("not a type" : String)

If the term's type is definitely not equal to the provided type, then elaboration succeeds:

[1, 2, 3]#eval ([1, 2, 3] !: String)

[1, 2, 3]

If the types match, an error is thrown:

#eval (Got unwanted type Nat5 !: Nat)

Got unwanted type Nat

The type equality check may fill in missing information, so sorry (which may have any type) is also rejected:

#eval (Got unwanted type Stringsorry !: String)

Got unwanted type String

Live ↪

Using Any Local Variable

Term elaborators have access to the expected type and to the local context. This can be used to create a term analogue of the assumption tactic.

The first step is to access the local context using getLocalHyps. It returns the context with the outermost bindings on the left, so it is traversed in reverse order. For each local assumption, a type is inferred with Meta.inferType. If it can be equal to the expected type, then the assumption is returned; if no assumption is suitable, then an error is produced.

syntax "anything!" : term

elab_rules <= expected
  | `(anything!) => do
    let hyps ← getLocalHyps
    for h in hyps.reverse do
      let t ← Meta.inferType h
      if (← Meta.isDefEq t expected) then return h

    throwError m!"No assumption in {hyps} has type {expected}"

The new syntax finds the function's bound variable:

7#eval (fun (n : Nat) => 2 + anything!) 5

It chooses the most recent suitable variable, as desired:

"It was y"#eval
  let x := "x"
  let y := "y"
  "It was " ++ y

"It was y"

When no assumption is suitable, it returns an error that describes the attempt:

#eval
  let x := Nat.zero
  let y := "hello"
  fun (f : Nat → Nat) =>
    (No assumption in [x, y, f] has type Int → Intanything! : Int → Int)

No assumption in [x, y, f] has type Int → Int

Because it uses unification, the natural number literal is chosen here, because numeric literals may have any type with an OfNat instance. Unfortunately, there is no OfNat instance for functions, so instance synthesis later fails.

#eval
  let x := failed to synthesize
  OfNat (Int → Int) 5
numerals are polymorphic in Lean, but the numeral `5` cannot be used in a context where the expected type is
  Int → Int
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.5
  let y := "hello"
  (anything! : Int → Int)

failed to synthesize
  OfNat (Int → Int) 5
numerals are polymorphic in Lean, but the numeral `5` cannot be used in a context where the expected type is
  Int → Int
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

Live ↪

21.6.3. Custom Tactics

Custom tactics are described in the section on tactics.