13.1. Custom Operators🔗

Lean supports custom infix, prefix, and postfix operators. New operators can be added by any Lean library, and the new operators have equal status to those that are part of the language. Each new operator is assigned an interpretation as a function, after which uses of the operator are translated into uses of the function. The operator's translation into a function call is referred to as its expansion. If this function is a type class method, then the resulting operator can be overloaded by defining instances of the class.

All operators have a precedence. Operator precedence determines the order of operations for unparenthesized expressions: because multiplication has a higher precedence than addition, 2 + 3 * 4 is equivalent to 2 + (3 * 4), and 2 * 3 + 4 is equivalent to (2 * 3) + 4. Infix operators additionally have an associativity that determines the meaning of a chain of operators that have the same precedence:

Left-associative

These operators nest to the left. Addition is left- associative, so 2 + 3 + 4 + 5 is equivalent to ((2 + 3) + 4) + 5.

Right-associative

These operators nest to the right. The product type is right-associative, so Nat × String × Unit × Option Int is equivalent to Nat × (String × (Unit × Option Int)).

Non-associative

Chaining these operators is a syntax error. Explicit parenthesization is required. Equality is non-associative, so the following is an error:

1 + 2 = 3 expected end of input= 2 + 1

The parser error is:

<example>:1:10: expected end of input

Precedence for Prefix and Infix Operators

The proposition ¬A ∧ B is equivalent to (¬A) ∧ B, because ¬ has a higher precedence than ∧. Because ∧ has higher precedence than = and is right-associative, ¬A ∧ B = (¬A) ∧ B is equivalent to ¬A ∧ ((B = ¬A) ∧ B).

Lean provides commands for defining new operators:

syntax

Non-associative infix operators are defined using Lean.Parser.Command.mixfix : commandinfix:

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.

A `docComment` 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. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind infix:prec ((name := ident))? ((priority := prio))? str => term

Left-associative infix operators are defined using Lean.Parser.Command.mixfix : commandinfixl:

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.

A `docComment` 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. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind infixl:prec ((name := ident))? ((priority := prio))? str => term

Right-associative infix operators are defined using Lean.Parser.Command.mixfix : commandinfixr:

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.

A `docComment` 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. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind infixr:prec ((name := ident))? ((priority := prio))? str => term

Prefix operators are defined using Lean.Parser.Command.mixfix : commandprefix:

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.

A `docComment` 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. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind prefix:prec ((name := ident))? ((priority := prio))? str => term

Postfix operators are defined using Lean.Parser.Command.mixfix : commandpostfix:

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.

A `docComment` 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. docComment?
      attributes?
      `attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`. attrKind postfix:prec ((name := ident))? ((priority := prio))? str => term

Each of these commands may be preceded by documentation comments and attributes. The documentation comment is shown when the user hovers their mouse over the operator, and attributes may invoke arbitrary metaprograms, just as for any other declaration. The attribute inherit_doc causes the documentation of the function that implements the operator to be re-used for the operator itself.

Operators interact with section scopes in the same manner as attributes. By default, operators are available in any module that transitively imports the one in which they are established, but they may be declared scoped or local to restrict their availability either to contexts in which the current namespace has been opened or to the current section scope, respectively.

Custom operators require a precedence specifier, following a colon. There is no default precedence to fall back to for custom operators.

Operators may be explicitly named. This name denotes the extension to Lean's syntax, and is primarily used for metaprogramming. If no name is explicitly provided, then Lean generates one based on the operator. The specifics of the assignment of this name should not be relied upon, both because the internal name assignment algorithm may change and because the introduction of similar operators in upstream dependencies may lead to a clash, in which case Lean will modify the assigned name until it is unique.

Assigned Operator Names

Given this infix operator:

infix:90 " ⤴ " => Option.getD

the internal name «term_⤴_» is assigned to the resulting parser extension.

Provided Operator Names

Given this infix operator:

infix:90 (name := getDOp) " ⤴ " => Option.getD

the resulting parser extension is named getDOp.

Inheriting Documentation

Given this infix operator:

@[inherit_doc]
infix:90 " ⤴ " => Option.getD

the resulting parser extension has the same documentation as Option.getD.

When multiple operators are defined that share the same syntax, Lean's parser attempts all of them. If more than one succeed, the one that used the most input is selected—this is called the local longest-match rule. In some cases, parsing multiple operators may succeed, all of them covering the same range of the input. In these cases, the operator's priority is used to select the appropriate result. Finally, if multiple operators with the same priority tie for the longest match, the parser saves all of the results, and the elaborator attempts each in turn, failing if elaboration does not succeed on exactly one of them.

Ambiguous Operators and Priorities

Defining an alternative implementation of + as Or requires only an infix operator declaration.

infix:65  " + " => Or

With this declaration, Lean attempts to elaborate addition both using the built-in syntax for HAdd.hAdd and the new syntax for Or:

True + False : Prop#check True + False

True + False : Prop

2 + 2 : Nat#check 2 + 2

2 + 2 : Nat

However, because the new operator is not associative, the local longest-match rule means that only HAdd.hAdd applies to an unparenthesized three-argument version:

#check failed to synthesize
  HAdd Prop Prop ?m.38
Additional diagnostic information may be available using the `set_option diagnostics true` command.True + False + True

failed to synthesize
  HAdd Prop Prop ?m.38
Additional diagnostic information may be available using the `set_option diagnostics true` command.

If the infix operator is declared with high priority, then Lean does not try the built-in HAdd.hAdd operator in ambiguous cases:

infix:65 (priority := high)  " + " => Or

True + False : Prop#check True + False

True + False : Prop

sorry + sorry : Prop#check failed to synthesize
  OfNat Prop 2
numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is
  Prop
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.2 + failed to synthesize
  OfNat Prop 2
numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is
  Prop
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.2

failed to synthesize
  OfNat Prop 2
numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is
  Prop
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

The new operator is not associative, so the local longest-match rule means that only HAdd.hAdd applies to the three-argument version:

#check failed to synthesize
  HAdd Prop Prop ?m.20
Additional diagnostic information may be available using the `set_option diagnostics true` command.True + False + True

failed to synthesize
  HAdd Prop Prop ?m.20
Additional diagnostic information may be available using the `set_option diagnostics true` command.

The actual operator is provided as a string literal. The new operator must satisfy the following requirements:

It must contain at least one character.
The first character may not be a single or double quote (' or "), unless the operator is ''.
It may not begin with a backtick (`) followed by a character that would be a valid prefix of a quoted name.
It may not begin with a digit.
It may not include internal whitespace.

The operator string literal may begin or end with a space. These are not part of the operator's syntax, and their presence does not require spaces around uses of the operator. However, the presence of spaces cause Lean to insert spaces when showing the operator to the user. Omitting them causes the operator's arguments to be displayed immediately next to the operator itself.

Finally, the operator's meaning is provided, separated from the operator by Lean.Parser.Command.mixfix : command=>. This may be any Lean term. Uses of the operator are desugared into function applications, with the provided term in the function position. Prefix and postfix operators apply the term to their single argument as an explicit argument. Infix operators apply the term to the left and right arguments, in that order. Other than its ability to accept arguments at each call site, there are no specific requirements imposed on the term. Operators may construct functions, so the term may expect more parameters than the operator. Implicit and instance-implicit parameters are resolved at each application site, which allows the operator to be defined by a type class method.

If the term consists either of a name from the global environment or of an application of such a name to one or more arguments, then Lean automatically generates an unexpander for the operator. This means that the operator will be displayed in proof states, error messages, and other output from Lean when the function term otherwise would have been displayed. Lean does not track whether the operator was used in the original term; it is inserted at every opportunity.

Custom Operators in Lean's Output

The function perhapsFactorial computes a factorial for a number if it's not too large.

def fact : Nat → Nat
  | 0 => 1
  | n+1 => (n + 1) * fact n

def perhapsFactorial (n : Nat) : Option Nat :=
  if n < 8 then some (fact n) else none

The postfix interrobang operator can be used to represent it.

postfix:90 "‽" => perhapsFactorial

When attempting to prove that ∀ n, n ≥ 8 → (perhapsFactorial n).isNone, the initial proof state uses the new operator, even though the theorem as written does not:

⊢ ∀ (n : Nat), n ≥ 8 → n‽.isNone = true