structure Lean.Parser.Category : Type

Auxiliary type used to represent syntax categories. We mainly use auxiliary definitions with this type to attach doc strings to syntax categories.

def Lean.Parser.Category.command : Category

command is the syntax category for things that appear at the top level of a lean file. For example, def foo := 1 is a command, as is namespace Foo and end Foo. Commands generally have an effect on the state of adding something to the environment (like a new definition), as well as commands like variable which modify future commands within a scope.

Equations

• Lean.Parser.Category.command = { }

def Lean.Parser.Category.term : Category

term is the builtin syntax category for terms. A term denotes an expression in lean's type theory, for example 2 + 2 is a term. The difference between Term and Expr is that the former is a kind of syntax, while the latter is the result of elaboration. For example by simp is also a Term, but it elaborates to different Exprs depending on the context.

Equations

• Lean.Parser.Category.term = { }

def Lean.Parser.Category.tactic : Category

tactic is the builtin syntax category for tactics. These appear after by in proofs, and they are programs that take in the proof context (the hypotheses in scope plus the type of the term to synthesize) and construct a term of the expected type. For example, simp is a tactic, used in:

example : 2 + 2 = 4 := by simp

Equations

• Lean.Parser.Category.tactic = { }

def Lean.Parser.Category.doElem : Category

doElem is a builtin syntax category for elements that can appear in the do notation. For example, let x ← e is a doElem, and a do block consists of a list of doElems.

Equations

• Lean.Parser.Category.doElem = { }

def Lean.Parser.Category.structInstFieldDecl : Category

structInstFieldDecl is the syntax category for value declarations for fields in structure instance notation. For example, the := 1 and | 0 => 0 | n + 1 => n in { x := 1, f | 0 => 0 | n + 1 => n } are in the structInstFieldDecl class.

Equations

• Lean.Parser.Category.structInstFieldDecl = { }

def Lean.Parser.Category.level : Category

level is a builtin syntax category for universe levels. This is the u in Sort u: it can contain max and imax, addition with constants, and variables.

Equations

• Lean.Parser.Category.level = { }

def Lean.Parser.Category.attr : Category

attr is a builtin syntax category for attributes. Declarations can be annotated with attributes using the @[...] notation.

Equations

• Lean.Parser.Category.attr = { }

def Lean.Parser.Category.stx : Category

stx is a builtin syntax category for syntax. This is the abbreviated parser notation used inside syntax and macro declarations.

Equations

• Lean.Parser.Category.stx = { }

def Lean.Parser.Category.prio : Category

prio is a builtin syntax category for priorities. Priorities are used in many different attributes. Higher numbers denote higher priority, and for example typeclass search will try high priority instances before low priority. In addition to literals like 37, you can also use low, mid, high, as well as add and subtract priorities.

Equations

• Lean.Parser.Category.prio = { }

def Lean.Parser.Category.prec : Category

prec is a builtin syntax category for precedences. A precedence is a value that expresses how tightly a piece of syntax binds: for example 1 + 2 * 3 is parsed as 1 + (2 * 3) because * has a higher precedence than +. Higher numbers denote higher precedence. In addition to literals like 37, there are some special named precedence levels:

• arg for the precedence of function arguments
• max for the highest precedence used in term parsers (not actually the maximum possible value)
• lead for the precedence of terms not supposed to be used as arguments and you can also add and subtract precedences.

Equations

• Lean.Parser.Category.prec = { }

DSL for specifying parser precedences and priorities

def Lean.Parser.Syntax.addPrec : TrailingParserDescr

Addition of precedences. This is normally used only for offsetting, e.g. max + 1.

Equations

• Lean.Parser.Syntax.addPrec = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.addPrec 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `prec 66))

def Lean.Parser.Syntax.subPrec : TrailingParserDescr

Subtraction of precedences. This is normally used only for offsetting, e.g. max - 1.

Equations

• Lean.Parser.Syntax.subPrec = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.subPrec 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `prec 66))

def Lean.Parser.Syntax.addPrio : TrailingParserDescr

Addition of priorities. This is normally used only for offsetting, e.g. default + 1.

Equations

• Lean.Parser.Syntax.addPrio = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.addPrio 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `prio 66))

def Lean.Parser.Syntax.subPrio : TrailingParserDescr

Subtraction of priorities. This is normally used only for offsetting, e.g. default - 1.

Equations

• Lean.Parser.Syntax.subPrio = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.subPrio 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `prio 66))

instance Lean.instCoeOutTSyntaxSyntax {ks : SyntaxNodeKinds} : CoeOut (TSyntax ks) Syntax

Equations

• Lean.instCoeOutTSyntaxSyntax = { coe := fun (stx : Lean.TSyntax ks) => stx.raw }

instance Lean.instCoeSyntaxNodeKindSyntaxNodeKinds : Coe SyntaxNodeKind SyntaxNodeKinds

Equations

• Lean.instCoeSyntaxNodeKindSyntaxNodeKinds = { coe := fun (k : Lean.SyntaxNodeKind) => [k] }

def precMax : Lean.ParserDescr

Maximum precedence used in term parsers, in particular for terms in function position (ident, paren, ...)

Equations

• precMax = Lean.ParserDescr.node `precMax 1024 (Lean.ParserDescr.nonReservedSymbol "max" false)

def precArg : Lean.ParserDescr

Precedence used for application arguments (do, by, ...).

Equations

• precArg = Lean.ParserDescr.node `precArg 1024 (Lean.ParserDescr.nonReservedSymbol "arg" false)

def precLead : Lean.ParserDescr

Precedence used for terms not supposed to be used as arguments (let, have, ...).

Equations

• precLead = Lean.ParserDescr.node `precLead 1024 (Lean.ParserDescr.nonReservedSymbol "lead" false)

def «prec(_)» : Lean.ParserDescr

Parentheses are used for grouping precedence expressions.

Equations

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

def precMin : Lean.ParserDescr

Minimum precedence used in term parsers.

Equations

• precMin = Lean.ParserDescr.node `precMin 1024 (Lean.ParserDescr.nonReservedSymbol "min" false)

def precMin1 : Lean.ParserDescr

(min+1) (we can only write min+1 after Meta.lean)

Equations

• precMin1 = Lean.ParserDescr.node `precMin1 1024 (Lean.ParserDescr.nonReservedSymbol "min1" false)

def termMax_prec : Lean.ParserDescr

max:prec as a term. It is equivalent to eval_prec max for eval_prec defined at Meta.lean. We use max_prec to workaround bootstrapping issues.

Equations

• termMax_prec = Lean.ParserDescr.node `termMax_prec 1024 (Lean.ParserDescr.symbol "max_prec")

def prioDefault : Lean.ParserDescr

The default priority default = 1000, which is used when no priority is set.

Equations

• prioDefault = Lean.ParserDescr.node `prioDefault 1024 (Lean.ParserDescr.nonReservedSymbol "default" false)

def prioLow : Lean.ParserDescr

The standardized "low" priority low = 100, for things that should be lower than default priority.

Equations

• prioLow = Lean.ParserDescr.node `prioLow 1024 (Lean.ParserDescr.nonReservedSymbol "low" false)

def prioMid : Lean.ParserDescr

The standardized "medium" priority mid = 500. This is lower than default, and higher than low.

Equations

• prioMid = Lean.ParserDescr.node `prioMid 1024 (Lean.ParserDescr.nonReservedSymbol "mid" false)

def prioHigh : Lean.ParserDescr

The standardized "high" priority high = 10000, for things that should be higher than default priority.

Equations

• prioHigh = Lean.ParserDescr.node `prioHigh 1024 (Lean.ParserDescr.nonReservedSymbol "high" false)

def «prio(_)» : Lean.ParserDescr

Parentheses are used for grouping priority expressions.

Equations

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

def «stx_+» : Lean.TrailingParserDescr

p+ is shorthand for many1(p). It uses parser p 1 or more times, and produces a nullNode containing the array of parsed results. This parser has arity 1.

If p has arity more than 1, it is auto-grouped in the items generated by the parser.

Equations

• «stx_+» = Lean.ParserDescr.trailingNode `«stx_+» 1023 1024 (Lean.ParserDescr.symbol "+")

def «stx_*» : Lean.TrailingParserDescr

p* is shorthand for many(p). It uses parser p 0 or more times, and produces a nullNode containing the array of parsed results. This parser has arity 1.

If p has arity more than 1, it is auto-grouped in the items generated by the parser.

Equations

• «stx_*» = Lean.ParserDescr.trailingNode `«stx_*» 1023 1024 (Lean.ParserDescr.symbol "*")

def stx_? : Lean.TrailingParserDescr

(p)? is shorthand for optional(p). It uses parser p 0 or 1 times, and produces a nullNode containing the array of parsed results. This parser has arity 1.

p is allowed to have arity n > 1 (in which case the node will have either 0 or n children), but if it has arity 0 then the result will be ambiguous.

Because ? is an identifier character, ident? will not work as intended. You have to write either ident ? or (ident)? for it to parse as the ? combinator applied to the ident parser.

Equations

• stx_? = Lean.ParserDescr.trailingNode `stx_? 1023 1024 (Lean.ParserDescr.symbol "?")

def «stx_<|>_» : Lean.TrailingParserDescr

p1 <|> p2 is shorthand for orelse(p1, p2), and parses either p1 or p2. It does not backtrack, meaning that if p1 consumes at least one token then p2 will not be tried. Therefore, the parsers should all differ in their first token. The atomic(p) parser combinator can be used to locally backtrack a parser. (For full backtracking, consider using extensible syntax classes instead.)

On success, if the inner parser does not generate exactly one node, it will be automatically wrapped in a group node, so the result will always be arity 1.

The <|> combinator does not generate a node of its own, and in particular does not tag the inner parsers to distinguish them, which can present a problem when reconstructing the parse. A well formed <|> parser should use disjoint node kinds for p1 and p2.

Equations

• «stx_<|>_» = Lean.ParserDescr.trailingNode `«stx_<|>_» 2 2 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <|> ") (Lean.ParserDescr.cat `stx 1))

def «stx_,*» : Lean.TrailingParserDescr

p,* is shorthand for sepBy(p, ","). It parses 0 or more occurrences of p separated by ,, that is: empty | p | p,p | p,p,p | ....

It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

Equations

• «stx_,*» = Lean.ParserDescr.trailingNode `«stx_,*» 1023 1024 (Lean.ParserDescr.symbol ",*")

def «stx_,+» : Lean.TrailingParserDescr

p,+ is shorthand for sepBy(p, ","). It parses 1 or more occurrences of p separated by ,, that is: p | p,p | p,p,p | ....

It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

Equations

• «stx_,+» = Lean.ParserDescr.trailingNode `«stx_,+» 1023 1024 (Lean.ParserDescr.symbol ",+")

def «stx_,*,?» : Lean.TrailingParserDescr

p,*,? is shorthand for sepBy(p, ",", allowTrailingSep). It parses 0 or more occurrences of p separated by ,, possibly including a trailing ,, that is: empty | p | p, | p,p | p,p, | p,p,p | ....

It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

Equations

• «stx_,*,?» = Lean.ParserDescr.trailingNode `«stx_,*,?» 1023 1024 (Lean.ParserDescr.symbol ",*,?")

def «stx_,+,?» : Lean.TrailingParserDescr

p,+,? is shorthand for sepBy1(p, ",", allowTrailingSep). It parses 1 or more occurrences of p separated by ,, possibly including a trailing ,, that is: p | p, | p,p | p,p, | p,p,p | ....

It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

Equations

• «stx_,+,?» = Lean.ParserDescr.trailingNode `«stx_,+,?» 1023 1024 (Lean.ParserDescr.symbol ",+,?")

def stx!_ : Lean.ParserDescr

!p parses the negation of p. That is, it fails if p succeeds, and otherwise parses nothing. It has arity 0.

Equations

• stx!_ = Lean.ParserDescr.node `stx!_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "!" false) (Lean.ParserDescr.cat `stx 1024))

def rawNatLit : Lean.ParserDescr

The nat_lit n macro constructs "raw numeric literals". This corresponds to the Expr.lit (.natVal n) constructor in the Expr data type.

Normally, when you write a numeral like #check 37, the parser turns this into an application of OfNat.ofNat to the raw literal 37 to cast it into the target type, even if this type is Nat (so the cast is the identity function). But sometimes it is necessary to talk about the raw numeral directly, especially when proving properties about the ofNat function itself.

Equations

• rawNatLit = Lean.ParserDescr.node `rawNatLit 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "nat_lit ") (Lean.ParserDescr.const `num))

def «term_∘_» : Lean.TrailingParserDescr

Function composition, usually written with the infix operator ∘. A new function is created from two existing functions, where one function's output is used as input to the other.

Examples:

• Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]
• (List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]

Conventions for notations in identifiers:

• The recommended spelling of ∘ in identifiers is comp.

Equations

• «term_∘_» = Lean.ParserDescr.trailingNode `«term_∘_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ ") (Lean.ParserDescr.cat `term 90))

def «term_×_» : Lean.TrailingParserDescr

The product type, usually written α × β. Product types are also called pair or tuple types. Elements of this type are pairs in which the first element is an α and the second element is a β.

Products nest to the right, so (x, y, z) : α × β × γ is equivalent to (x, (y, z)) : α × (β × γ).

Conventions for notations in identifiers:

• The recommended spelling of × in identifiers is Prod.

Equations

• «term_×_» = Lean.ParserDescr.trailingNode `«term_×_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " × ") (Lean.ParserDescr.cat `term 35))

def «term_×'_» : Lean.TrailingParserDescr

A product type in which the types may be propositions, usually written α ×' β.

This type is primarily used internally and as an implementation detail of proof automation. It is rarely useful in hand-written code.

Conventions for notations in identifiers:

• The recommended spelling of ×' in identifiers is PProd.

Equations

• «term_×'_» = Lean.ParserDescr.trailingNode `«term_×'_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×' ") (Lean.ParserDescr.cat `term 35))

def «term_∣_» : Lean.TrailingParserDescr

Divisibility. a ∣ b (typed as \|) means that there is some c such that b = a * c.

Conventions for notations in identifiers:

• The recommended spelling of ∣ in identifiers is dvd.

Equations

• «term_∣_» = Lean.ParserDescr.trailingNode `«term_∣_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∣ ") (Lean.ParserDescr.cat `term 51))

def «term_|||_» : Lean.TrailingParserDescr

a ||| b computes the bitwise OR of a and b. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of ||| in identifiers is or.

Equations

• «term_|||_» = Lean.ParserDescr.trailingNode `«term_|||_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ||| ") (Lean.ParserDescr.cat `term 56))

def «term_^^^_» : Lean.TrailingParserDescr

a ^^^ b computes the bitwise XOR of a and b. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of ^^^ in identifiers is xor.

Equations

• «term_^^^_» = Lean.ParserDescr.trailingNode `«term_^^^_» 58 58 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^^^ ") (Lean.ParserDescr.cat `term 59))

def «term_&&&_» : Lean.TrailingParserDescr

a &&& b computes the bitwise AND of a and b. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of &&& in identifiers is and.

Equations

• «term_&&&_» = Lean.ParserDescr.trailingNode `«term_&&&_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " &&& ") (Lean.ParserDescr.cat `term 61))

def «term_+_» : Lean.TrailingParserDescr

a + b computes the sum of a and b. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of + in identifiers is add.

Equations

• «term_+_» = Lean.ParserDescr.trailingNode `«term_+_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `term 66))

def «term_-_» : Lean.TrailingParserDescr

a - b computes the difference of a and b. The meaning of this notation is type-dependent.

• For natural numbers, this operator saturates at 0: a - b = 0 when a ≤ b.

Conventions for notations in identifiers:

• The recommended spelling of - in identifiers is sub (when used as a binary operator).

Equations

• «term_-_» = Lean.ParserDescr.trailingNode `«term_-_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `term 66))

def «term_*_» : Lean.TrailingParserDescr

a * b computes the product of a and b. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of * in identifiers is mul.

Equations

• «term_*_» = Lean.ParserDescr.trailingNode `«term_*_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " * ") (Lean.ParserDescr.cat `term 71))

def «term_/_» : Lean.TrailingParserDescr

a / b computes the result of dividing a by b. The meaning of this notation is type-dependent.

• For most types like Nat, Int, Rat, Real, a / 0 is defined to be 0.
• For Nat, a / b rounds downwards.
• For Int, a / b rounds downwards if b is positive or upwards if b is negative. It is implemented as Int.ediv, the unique function satisfying a % b + b * (a / b) = a and 0 ≤ a % b < natAbs b for b ≠ 0. Other rounding conventions are available using the functions Int.fdiv (floor rounding) and Int.tdiv (truncation rounding).
• For Float, a / 0 follows the IEEE 754 semantics for division, usually resulting in inf or nan.

Conventions for notations in identifiers:

• The recommended spelling of / in identifiers is div.

Equations

• «term_/_» = Lean.ParserDescr.trailingNode `«term_/_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " / ") (Lean.ParserDescr.cat `term 71))

def «term_%_» : Lean.TrailingParserDescr

a % b computes the remainder upon dividing a by b. The meaning of this notation is type-dependent.

• For Nat and Int it satisfies a % b + b * (a / b) = a, and a % 0 is defined to be a.

Conventions for notations in identifiers:

• The recommended spelling of % in identifiers is mod.

Equations

• «term_%_» = Lean.ParserDescr.trailingNode `«term_%_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " % ") (Lean.ParserDescr.cat `term 71))

def «term_<<<_» : Lean.TrailingParserDescr

a <<< b computes a shifted to the left by b places. The meaning of this notation is type-dependent.

• On Nat, this is equivalent to a * 2 ^ b.
• On UInt8 and other fixed width unsigned types, this is the same but truncated to the bit width.

Conventions for notations in identifiers:

• The recommended spelling of <<< in identifiers is shiftLeft.

Equations

• «term_<<<_» = Lean.ParserDescr.trailingNode `«term_<<<_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <<< ") (Lean.ParserDescr.cat `term 76))

def «term_>>>_» : Lean.TrailingParserDescr

a >>> b computes a shifted to the right by b places. The meaning of this notation is type-dependent.

• On Nat and fixed width unsigned types like UInt8, this is equivalent to a / 2 ^ b.

Conventions for notations in identifiers:

• The recommended spelling of >>> in identifiers is shiftRight.

Equations

• «term_>>>_» = Lean.ParserDescr.trailingNode `«term_>>>_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >>> ") (Lean.ParserDescr.cat `term 76))

def «term_^_» : Lean.TrailingParserDescr

a ^ b computes a to the power of b. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of ^ in identifiers is pow.

Equations

• «term_^_» = Lean.ParserDescr.trailingNode `«term_^_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^ ") (Lean.ParserDescr.cat `term 80))

def «term_++_» : Lean.TrailingParserDescr

a ++ b is the result of concatenation of a and b, usually read "append". The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of ++ in identifiers is append.

Equations

• «term_++_» = Lean.ParserDescr.trailingNode `«term_++_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ ") (Lean.ParserDescr.cat `term 66))

def «term-_» : Lean.ParserDescr

-a computes the negative or opposite of a. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of - in identifiers is neg (when used as a unary operator).

Equations

• «term-_» = Lean.ParserDescr.node `«term-_» 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "-") (Lean.ParserDescr.cat `term 75))

def «term~~~_» : Lean.ParserDescr

The implementation of ~~~a : α.

Conventions for notations in identifiers:

• The recommended spelling of ~~~ in identifiers is not.

Equations

• «term~~~_» = Lean.ParserDescr.node `«term~~~_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~~~") (Lean.ParserDescr.cat `term 100))

def «term_⁻¹» : Lean.TrailingParserDescr

a⁻¹ computes the inverse of a. The meaning of this notation is type-dependent.

Equations

• «term_⁻¹» = Lean.ParserDescr.trailingNode `«term_⁻¹» 1024 1024 (Lean.ParserDescr.symbol "⁻¹")

def «term_•_» : Lean.TrailingParserDescr

a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

Conventions for notations in identifiers:

• The recommended spelling of • in identifiers is smul.

Equations

• «term_•_» = Lean.ParserDescr.trailingNode `«term_•_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " • ") (Lean.ParserDescr.cat `term 73))

Remark: the infix commands above ensure a delaborator is generated for each relations. We redefine the macros below to be able to use the auxiliary binop% elaboration helper for binary operators. It addresses issue #382.

We have a macro to make x • y notation participate in the expression tree elaborator, like other arithmetic expressions such as +, *, /, ^, =, inequalities, etc. The macro is using the leftact% elaborator introduced in this RFC.

As a concrete example of the effect of this macro, consider

variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
#check m + r • n

Without the macro, the expression would elaborate as m + ↑(r • n : ↑N) : M. With the macro, the expression elaborates as m + r • (↑n : M) : M. To get the first interpretation, one can write m + (r • n :).

Here is a quick review of the expression tree elaborator:

1. It builds up an expression tree of all the immediately accessible operations that are marked with binop%, unop%, leftact%, rightact%, binrel%, etc.
2. It elaborates every leaf term of this tree (without an expected type, so as if it were temporarily wrapped in (... :)).
3. Using the types of each elaborated leaf, it computes a supremum type they can all be coerced to, if such a supremum exists.
4. It inserts coercions around leaf terms wherever needed.

The hypothesis is that individual expression trees tend to be calculations with respect to a single algebraic structure.

Note(kmill): If we were to remove HSMul and switch to using SMul directly, then the expression tree elaborator would not be able to insert coercions within the right operand; they would likely appear as ↑(x • y) rather than x • ↑y, unlike other arithmetic operations.

def «term_<=_» : Lean.TrailingParserDescr

The less-equal relation: x ≤ y

Conventions for notations in identifiers:

• The recommended spelling of <= in identifiers is le (prefer ≤ over <=).

Equations

• «term_<=_» = Lean.ParserDescr.trailingNode `«term_<=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <= ") (Lean.ParserDescr.cat `term 51))

def «term_≤_» : Lean.TrailingParserDescr

The less-equal relation: x ≤ y

Conventions for notations in identifiers:

• The recommended spelling of ≤ in identifiers is le.

Equations

• «term_≤_» = Lean.ParserDescr.trailingNode `«term_≤_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ ") (Lean.ParserDescr.cat `term 51))

def «term_<_» : Lean.TrailingParserDescr

The less-than relation: x < y

Conventions for notations in identifiers:

• The recommended spelling of < in identifiers is lt.

Equations

• «term_<_» = Lean.ParserDescr.trailingNode `«term_<_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " < ") (Lean.ParserDescr.cat `term 51))

def «term_>=_» : Lean.TrailingParserDescr

a ≥ b is an abbreviation for b ≤ a.

Conventions for notations in identifiers:

• The recommended spelling of >= in identifiers is ge (prefer ≥ over >=).

Equations

• «term_>=_» = Lean.ParserDescr.trailingNode `«term_>=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >= ") (Lean.ParserDescr.cat `term 51))

def «term_≥_» : Lean.TrailingParserDescr

a ≥ b is an abbreviation for b ≤ a.

Conventions for notations in identifiers:

• The recommended spelling of ≥ in identifiers is ge.

Equations

• «term_≥_» = Lean.ParserDescr.trailingNode `«term_≥_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ ") (Lean.ParserDescr.cat `term 51))

def «term_>_» : Lean.TrailingParserDescr

a > b is an abbreviation for b < a.

Conventions for notations in identifiers:

• The recommended spelling of > in identifiers is gt.

Equations

• «term_>_» = Lean.ParserDescr.trailingNode `«term_>_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " > ") (Lean.ParserDescr.cat `term 51))

def «term_=_» : Lean.TrailingParserDescr

The equality relation. It has one introduction rule, Eq.refl. We use a = b as notation for Eq a b. A fundamental property of equality is that it is an equivalence relation.

variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd

Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given h1 : a = b and h2 : p a, we can construct a proof for p b using substitution: Eq.subst h1 h2. Example:

example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2

The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t. For more information: Equality

Conventions for notations in identifiers:

• The recommended spelling of = in identifiers is eq.

Equations

• «term_=_» = Lean.ParserDescr.trailingNode `«term_=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " = ") (Lean.ParserDescr.cat `term 51))

def «term_==_» : Lean.TrailingParserDescr

Boolean equality, notated as a == b.

Conventions for notations in identifiers:

• The recommended spelling of == in identifiers is beq.

Equations

• «term_==_» = Lean.ParserDescr.trailingNode `«term_==_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " == ") (Lean.ParserDescr.cat `term 51))

def «term_≍_» : Lean.TrailingParserDescr

Heterogeneous equality. HEq a b asserts that a and b have the same type, and casting a across the equality yields b, and vice versa.

You should avoid using this type if you can. Heterogeneous equality does not have all the same properties as Eq, because the assumption that the types of a and b are equal is often too weak to prove theorems of interest. One important non-theorem is the analogue of congr: If HEq f g and HEq x y and f x and g y are well typed it does not follow that HEq (f x) (g y). (This does follow if you have f = g instead.) However if a and b have the same type then a = b and HEq a b are equivalent.

Equations

• «term_≍_» = Lean.ParserDescr.trailingNode `«term_≍_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≍ ") (Lean.ParserDescr.cat `term 51))

Remark: the infix commands above ensure a delaborator is generated for each relations. We redefine the macros below to be able to use the auxiliary binrel% elaboration helper for binary relations. It has better support for applying coercions. For example, suppose we have binrel% Eq n i where n : Nat and i : Int. The default elaborator fails because we don't have a coercion from Int to Nat, but binrel% succeeds because it also tries a coercion from Nat to Int even when the nat occurs before the int.

def «term_/\_» : Lean.TrailingParserDescr

And a b, or a ∧ b, is the conjunction of propositions. It can be constructed and destructed like a pair: if ha : a and hb : b then ⟨ha, hb⟩ : a ∧ b, and if h : a ∧ b then h.left : a and h.right : b.

Conventions for notations in identifiers:

• The recommended spelling of /\ in identifiers is and (prefer ∧ over /\).

Equations

• «term_/\_» = Lean.ParserDescr.trailingNode `«term_/\_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /\\ ") (Lean.ParserDescr.cat `term 35))

def «term_∧_» : Lean.TrailingParserDescr

And a b, or a ∧ b, is the conjunction of propositions. It can be constructed and destructed like a pair: if ha : a and hb : b then ⟨ha, hb⟩ : a ∧ b, and if h : a ∧ b then h.left : a and h.right : b.

Conventions for notations in identifiers:

• The recommended spelling of ∧ in identifiers is and.

Equations

• «term_∧_» = Lean.ParserDescr.trailingNode `«term_∧_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `term 35))

def «term_\/_» : Lean.TrailingParserDescr

Or a b, or a ∨ b, is the disjunction of propositions. There are two constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b, and you can use match or cases to destruct an Or assumption into the two cases.

Conventions for notations in identifiers:

• The recommended spelling of \/ in identifiers is or (prefer ∨ over \/).

Equations

• «term_\/_» = Lean.ParserDescr.trailingNode `«term_\/_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\/ ") (Lean.ParserDescr.cat `term 30))

def «term_∨_» : Lean.TrailingParserDescr

Or a b, or a ∨ b, is the disjunction of propositions. There are two constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b, and you can use match or cases to destruct an Or assumption into the two cases.

Conventions for notations in identifiers:

• The recommended spelling of ∨ in identifiers is or.

Equations

• «term_∨_» = Lean.ParserDescr.trailingNode `«term_∨_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `term 30))

def «term¬_» : Lean.ParserDescr

Not p, or ¬p, is the negation of p. It is defined to be p → False, so if your goal is ¬p you can use intro h to turn the goal into h : p ⊢ False, and if you have hn : ¬p and h : p then hn h : False and (hn h).elim will prove anything. For more information: Propositional Logic

Conventions for notations in identifiers:

• The recommended spelling of ¬ in identifiers is not.

Equations

• «term¬_» = Lean.ParserDescr.node `«term¬_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `term 40))

def «term_&&_» : Lean.TrailingParserDescr

Boolean “and”, also known as conjunction. and x y can be written x && y.

The corresponding propositional connective is And : Prop → Prop → Prop, written with the ∧ operator.

The Boolean and is a @[macro_inline] function in order to give it short-circuiting evaluation: if x is false then y is not evaluated at runtime.

Conventions for notations in identifiers:

• The recommended spelling of && in identifiers is and.

Equations

• «term_&&_» = Lean.ParserDescr.trailingNode `«term_&&_» 35 35 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " && ") (Lean.ParserDescr.cat `term 36))

def «term_||_» : Lean.TrailingParserDescr

Boolean “or”, also known as disjunction. or x y can be written x || y.

The corresponding propositional connective is Or : Prop → Prop → Prop, written with the ∨ operator.

The Boolean or is a @[macro_inline] function in order to give it short-circuiting evaluation: if x is true then y is not evaluated at runtime.

Conventions for notations in identifiers:

• The recommended spelling of || in identifiers is or.

Equations

• «term_||_» = Lean.ParserDescr.trailingNode `«term_||_» 30 30 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " || ") (Lean.ParserDescr.cat `term 31))

def term!_ : Lean.ParserDescr

Boolean negation, also known as Boolean complement. not x can be written !x.

This is a function that maps the value true to false and the value false to true. The propositional connective is Not : Prop → Prop.

Conventions for notations in identifiers:

• The recommended spelling of ! in identifiers is not.

Equations

• term!_ = Lean.ParserDescr.node `term!_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "!") (Lean.ParserDescr.cat `term 40))

def «term_∈_» : Lean.TrailingParserDescr

The membership relation a ∈ s : Prop where a : α, s : γ.

Conventions for notations in identifiers:

• The recommended spelling of ∈ in identifiers is mem.

Equations

• «term_∈_» = Lean.ParserDescr.trailingNode `«term_∈_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ ") (Lean.ParserDescr.cat `term 50))

def «term_∉_» : Lean.TrailingParserDescr

a ∉ b is negated elementhood. It is notation for ¬ (a ∈ b).

Conventions for notations in identifiers:

• The recommended spelling of ∉ in identifiers is not_mem.

Equations

• «term_∉_» = Lean.ParserDescr.trailingNode `«term_∉_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∉ ") (Lean.ParserDescr.cat `term 50))

def «term_::_» : Lean.TrailingParserDescr

The list whose first element is head, where tail is the rest of the list. Usually written head :: tail.

Conventions for notations in identifiers:

• The recommended spelling of :: in identifiers is cons.

Equations

• «term_::_» = Lean.ParserDescr.trailingNode `«term_::_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))

def «term_<$>_» : Lean.TrailingParserDescr

Applies a function inside a functor. This is used to overload the <$> operator.

When mapping a constant function, use Functor.mapConst instead, because it may be more efficient.

Conventions for notations in identifiers:

• The recommended spelling of <$> in identifiers is map.

Equations

• «term_<$>_» = Lean.ParserDescr.trailingNode `«term_<$>_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <$> ") (Lean.ParserDescr.cat `term 100))

def «term_>>=_» : Lean.TrailingParserDescr

Sequences two computations, allowing the second to depend on the value computed by the first.

If x : m α and f : α → m β, then x >>= f : m β represents the result of executing x to get a value of type α and then passing it to f.

Conventions for notations in identifiers:

• The recommended spelling of >>= in identifiers is bind.

Equations

• «term_>>=_» = Lean.ParserDescr.trailingNode `«term_>>=_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >>= ") (Lean.ParserDescr.cat `term 56))

def «term_<|>_» : Lean.TrailingParserDescr

a <|> b executes a and returns the result, unless it fails in which case it executes and returns b. Because b is not always executed, it is passed as a thunk so it can be forced only when needed. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of <|> in identifiers is orElse.

Equations

• «term_<|>_» = Lean.ParserDescr.trailingNode `«term_<|>_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <|> ") (Lean.ParserDescr.cat `term 20))

def «term_>>_» : Lean.TrailingParserDescr

a >> b executes a, ignores the result, and then executes b. If a fails then b is not executed. Because b is not always executed, it is passed as a thunk so it can be forced only when needed. The meaning of this notation is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of >> in identifiers is andThen.

Equations

• «term_>>_» = Lean.ParserDescr.trailingNode `«term_>>_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >> ") (Lean.ParserDescr.cat `term 60))

def «term_<*>_» : Lean.TrailingParserDescr

The implementation of the <*> operator.

In a monad, mf <*> mx is the same as do let f ← mf; x ← mx; pure (f x): it evaluates the function first, then the argument, and applies one to the other.

To avoid surprising evaluation semantics, mx is taken "lazily", using a Unit → f α function.

Conventions for notations in identifiers:

• The recommended spelling of <*> in identifiers is seq.

Equations

• «term_<*>_» = Lean.ParserDescr.trailingNode `«term_<*>_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <*> ") (Lean.ParserDescr.cat `term 61))

def «term_<*_» : Lean.TrailingParserDescr

Sequences the effects of two terms, discarding the value of the second. This function is usually invoked via the <* operator.

Given x : f α and y : f β, x <* y runs x, then runs y, and finally returns the result of x.

The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from f.

Conventions for notations in identifiers:

• The recommended spelling of <* in identifiers is seqLeft.

Equations

• «term_<*_» = Lean.ParserDescr.trailingNode `«term_<*_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <* ") (Lean.ParserDescr.cat `term 61))

def «term_*>_» : Lean.TrailingParserDescr

Sequences the effects of two terms, discarding the value of the first. This function is usually invoked via the *> operator.

Given x : f α and y : f β, x *> y runs x, then runs y, and finally returns the result of y.

The evaluation of the second argument is delayed by wrapping it in a function, enabling “short-circuiting” behavior from f.

Conventions for notations in identifiers:

• The recommended spelling of *> in identifiers is seqRight.

Equations

• «term_*>_» = Lean.ParserDescr.trailingNode `«term_*>_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *> ") (Lean.ParserDescr.cat `term 61))

def Lean.binderIdent : ParserDescr

binderIdent matches an ident or a _. It is used for identifiers in binding position, where _ means that the value should be left unnamed and inaccessible.

Equations

• Lean.binderIdent = Lean.ParserDescr.nodeWithAntiquot "binderIdent" `Lean.binderIdent (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.const `hole))

def Lean.Parser.Tactic.caseArg : ParserDescr

A case tag argument has the form tag x₁ ... xₙ; it refers to tag tag and renames the last n hypotheses to x₁ ... xₙ.

Equations

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

def termDepIfThenElse : Lean.ParserDescr

"Dependent" if-then-else, normally written via the notation if h : c then t(h) else e(h), is sugar for dite c (fun h => t(h)) (fun h => e(h)), and it is the same as if c then t else e except that t is allowed to depend on a proof h : c, and e can depend on h : ¬c. (Both branches use the same name for the hypothesis, even though it has different types in the two cases.)

We use this to be able to communicate the if-then-else condition to the branches. For example, Array.get arr i h expects a proof h : i < arr.size in order to avoid a bounds check, so you can write if h : i < arr.size then arr.get i h else ... to avoid the bounds check inside the if branch. (Of course in this case we have only lifted the check into an explicit if, but we could also use this proof multiple times or derive i < arr.size from some other proposition that we are checking in the if.)

Equations

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

def termIfThenElse : Lean.ParserDescr

if c then t else e is notation for ite c t e, "if-then-else", which decides to return t or e depending on whether c is true or false. The explicit argument c : Prop does not have any actual computational content, but there is an additional [Decidable c] argument synthesized by typeclass inference which actually determines how to evaluate c to true or false. Write if h : c then t else e instead for a "dependent if-then-else" dite, which allows t/e to use the fact that c is true/false.

Equations

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

def termIfLet : Lean.ParserDescr

if let pat := d then t else e is a shorthand syntax for:

match d with
| pat => t
| _ => e

It matches d against the pattern pat and the bindings are available in t. If the pattern does not match, it returns e instead.

Equations

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

def boolIfThenElse : Lean.ParserDescr

The conditional function.

cond c x y is the same as if c then x else y, but optimized for a Boolean condition rather than a decidable proposition. It can also be written using the notation bif c then x else y.

Just like ite, cond is declared @[macro_inline], which causes applications of cond to be unfolded. As a result, x and y are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated.

Equations

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

def «term_<|_» : Lean.TrailingParserDescr

Haskell-like pipe operator <|. f <| x means the same as the same as f x, except that it parses x with lower precedence, which means that f <| g <| x is interpreted as f (g x) rather than (f g) x.

Equations

• «term_<|_» = Lean.ParserDescr.trailingNode `«term_<|_» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <| ") (Lean.ParserDescr.cat `term 10))

def «term_|>_» : Lean.TrailingParserDescr

Haskell-like pipe operator |>. x |> f means the same as the same as f x, and it chains such that x |> f |> g is interpreted as g (f x).

Equations

• «term_|>_» = Lean.ParserDescr.trailingNode `«term_|>_» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " |> ") (Lean.ParserDescr.cat `term 11))

def «term_$__» : Lean.TrailingParserDescr

Alternative syntax for <|. f $ x means the same as the same as f x, except that it parses x with lower precedence, which means that f $ g $ x is interpreted as f (g x) rather than (f g) x.

Equations

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

def «term{_:_//_}» : Lean.ParserDescr

All the elements of a type that satisfy a predicate.

Subtype p, usually written { x : α // p x } or { x // p x }, contains all elements x : α for which p x is true. Its constructor is a pair of the value and the proof that it satisfies the predicate. In run-time code, { x : α // p x } is represented identically to α.

There is a coercion from { x : α // p x } to α, so elements of a subtype may be used where the underlying type is expected.

Examples:

• { n : Nat // n % 2 = 0 } is the type of even numbers.
• { xs : Array String // xs.size = 5 } is the type of arrays with five Strings.
• Given xs : List α, List { x : α // x ∈ xs } is the type of lists in which all elements are contained in xs.

Conventions for notations in identifiers:

• The recommended spelling of { x // p x } in identifiers is subtype.

Equations

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

def termWithout_expected_type_ : Lean.ParserDescr

without_expected_type t instructs Lean to elaborate t without an expected type. Recall that terms such as match ... with ... and ⟨...⟩ will postpone elaboration until expected type is known. So, without_expected_type is not effective in this case.

Equations

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

def Lean.byElab : ParserDescr

• The by_elab doSeq expression runs the doSeq as a TermElabM Expr to synthesize the expression.
• by_elab fun expectedType? => do doSeq receives the expected type (an Option Expr) as well.

Equations

• Lean.byElab = Lean.ParserDescr.node `Lean.byElab 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "by_elab ") (Lean.ParserDescr.const `doSeq))

def Lean.Parser.Category.rawStx : Category

Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer. The only accepted parser for this category is an antiquotation.

Equations

• Lean.Parser.Category.rawStx = { }

def Lean.rawStx.quot : ParserDescr

Equations

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

instance Lean.instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStr1Nil : Coe Syntax (TSyntax `rawStx)

Equations

• Lean.instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStr1Nil = { coe := fun (stx : Lean.Syntax) => { raw := stx } }

def Lean.withAnnotateTerm : ParserDescr

with_annotate_term stx e annotates the lexical range of stx : Syntax with term info for e.

Equations

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

def Lean.modCast : ParserDescr

Normalize casts in an expression using the same method as the norm_cast tactic.

Equations

• Lean.modCast = Lean.ParserDescr.node `Lean.modCast 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "mod_cast ") (Lean.ParserDescr.cat `term 0))

def Lean.deprecated : ParserDescr

The attribute @[deprecated] on a declaration indicates that the declaration is discouraged for use in new code, and/or should be migrated away from in existing code. It may be removed in a future version of the library.

• @[deprecated myBetterDef] means that myBetterDef is the suggested replacement.
• @[deprecated myBetterDef "use myBetterDef instead"] allows customizing the deprecation message.
• @[deprecated (since := "2024-04-21")] records when the deprecation was first applied.

Equations

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

def Lean.Attr.coe : ParserDescr

The @[coe] attribute on a function (which should also appear in a instance : Coe A B := ⟨myFn⟩ declaration) allows the delaborator to show applications of this function as ↑ when printing expressions.

Equations

• Lean.Attr.coe = Lean.ParserDescr.node `Lean.Attr.coe 1024 (Lean.ParserDescr.nonReservedSymbol "coe" false)

def Lean.command_code_action : ParserDescr

This attribute marks a code action, which is used to suggest new tactics or replace existing ones.

• @[command_code_action kind]: This is a code action which applies to applications of the command kind (a command syntax kind), which can replace the command or insert things before or after it.

• @[command_code_action kind₁ kind₂]: shorthand for @[command_code_action kind₁, command_code_action kind₂].

• @[command_code_action]: This is a command code action that applies to all commands. Use sparingly.

Equations

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

def Lean.builtin_command_code_action : ParserDescr

Builtin command code action. See command_code_action.

Equations

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

def Lean.includeStr : ParserDescr

When parent_dir contains the current Lean file, include_str "path" / "to" / "file" becomes a string literal with the contents of the file at "parent_dir" / "path" / "to" / "file". If this file cannot be read, elaboration fails.

Equations

• Lean.includeStr = Lean.ParserDescr.node `Lean.includeStr 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "include_str ") (Lean.ParserDescr.cat `term 0))

def Lean.runCmd : ParserDescr

The run_cmd doSeq command executes code in CommandElabM Unit. This is the same as #eval show CommandElabM Unit from discard do doSeq.

Equations

• Lean.runCmd = Lean.ParserDescr.node `Lean.runCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "run_cmd ") (Lean.ParserDescr.const `doSeq))

def Lean.runElab : ParserDescr

The run_elab doSeq command executes code in TermElabM Unit. This is the same as #eval show TermElabM Unit from discard do doSeq.

Equations

• Lean.runElab = Lean.ParserDescr.node `Lean.runElab 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "run_elab ") (Lean.ParserDescr.const `doSeq))

def Lean.runMeta : ParserDescr

The run_meta doSeq command executes code in MetaM Unit. This is the same as #eval show MetaM Unit from do discard doSeq.

(This is effectively a synonym for run_elab since MetaM lifts to TermElabM.)

Equations

• Lean.runMeta = Lean.ParserDescr.node `Lean.runMeta 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "run_meta ") (Lean.ParserDescr.const `doSeq))

def Lean.reduceCmd : ParserDescr

#reduce <expression> reduces the expression <expression> to its normal form. This involves applying reduction rules until no further reduction is possible.

By default, proofs and types within the expression are not reduced. Use modifiers (proofs := true) and (types := true) to reduce them. Recall that propositions are types in Lean.

Warning: This can be a computationally expensive operation, especially for complex expressions.

Consider using #eval <expression> for simple evaluation/execution of expressions.

Equations

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

def Lean.guardMsgsFilterAction : ParserDescr

Equations

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

def Lean.guardMsgsFilterSeverity : ParserDescr

Equations

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

def Lean.guardMsgsFilter : ParserDescr

A message filter specification for #guard_msgs.

• info, warning, error: capture (non-trace) messages with the given severity level.
• trace: captures trace messages
• all: capture all messages.

The filters can be prefixed with

• check (the default): capture and check the message
• drop: drop the message
• pass: let the message pass through

If no filter is specified, check all is assumed. Otherwise, these filters are processed in left-to-right order, with an implicit pass all at the end.

Equations

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

def Lean.guardMsgsWhitespaceArg : ParserDescr

Equations

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

def Lean.guardMsgsWhitespace : ParserDescr

Whitespace handling for #guard_msgs:

• whitespace := exact requires an exact whitespace match.
• whitespace := normalized converts all newline characters to a space before matching (the default). This allows breaking long lines.
• whitespace := lax collapses whitespace to a single space before matching. In all cases, leading and trailing whitespace is trimmed before matching.

Equations

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

def Lean.guardMsgsOrderingArg : ParserDescr

Equations

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

def Lean.guardMsgsOrdering : ParserDescr

Message ordering for #guard_msgs:

• ordering := exact uses the exact ordering of the messages (the default).
• ordering := sorted sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering.

Equations

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

def Lean.guardMsgsSpecElt : ParserDescr

Equations

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

def Lean.guardMsgsSpec : ParserDescr

Equations

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

def Lean.guardMsgsCmd : ParserDescr

/-- ... -/ #guard_msgs in cmd captures the messages generated by the command cmd and checks that they match the contents of the docstring.

Basic example:

/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x

This checks that there is such an error and then consumes the message.

By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings:

/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry

or only errors

#guard_msgs(error) in
example : α := sorry

In the previous example, since warnings are not captured there is a warning on sorry. We can drop the warning completely with

#guard_msgs(error, drop warning) in
example : α := sorry

In general, #guard_msgs accepts a comma-separated list of configuration clauses in parentheses:

#guard_msgs (configElt,*) in cmd

By default, the configuration list is (check all, whitespace := normalized, ordering := exact).

Message filters select messages by severity:

• info, warning, error: (non-trace) messages with the given severity level.
• trace: trace messages
• all: all messages.

The filters can be prefixed with the action to take:

• check (the default): capture and check the message
• drop: drop the message
• pass: let the message pass through

If no filter is specified, check all is assumed. Otherwise, these filters are processed in left-to-right order, with an implicit pass all at the end.

Whitespace handling (after trimming leading and trailing whitespace):

• whitespace := exact requires an exact whitespace match.
• whitespace := normalized converts all newline characters to a space before matching (the default). This allows breaking long lines.
• whitespace := lax collapses whitespace to a single space before matching.

Message ordering:

• ordering := exact uses the exact ordering of the messages (the default).
• ordering := sorted sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering.

For example, #guard_msgs (error, drop all) in cmd means to check warnings and drop everything else.

The command elaborator has special support for #guard_msgs for linting. The #guard_msgs itself wants to capture linter warnings, so it elaborates the command it is attached to as if it were a top-level command. However, the command elaborator runs linters for all top-level commands, which would include #guard_msgs itself, and would cause duplicate and/or uncaptured linter warnings. The top-level command elaborator only runs the linters if #guard_msgs is not present.

Equations

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

def Lean.infoTreesCmd : ParserDescr

Format and print the info trees for a given command. This is mostly useful for debugging info trees.

Equations

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

def Lean.setPremiseSelectorCmd : ParserDescr

Specify a premise selection engine. Note that Lean does not ship a default premise selection engine, so this is only useful in conjunction with a downstream package which provides one.

Equations

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

def Lean.Parser.checkTactic : ParserDescr

#check_tactic t ~> r by commands runs the tactic sequence commands on a goal with t and sees if the resulting expression has reduced it to r.

Equations

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

def Lean.Parser.checkTacticFailure : ParserDescr

#check_tactic_failure t by tac runs the tactic tac on a goal with t and verifies it fails.

Equations

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

def Lean.Parser.checkSimp : ParserDescr

#check_simp t ~> r checks simp reduces t to r.

Equations

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

def Lean.Parser.checkSimpFailure : ParserDescr

#check_simp t !~> checks simp fails on reducing t.

Equations

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

def Lean.Parser.timeCmd : ParserDescr

Time the elaboration of a command, and print the result (in milliseconds).

Example usage:

set_option maxRecDepth 100000 in
#time example : (List.range 500).length = 500 := rfl

Equations

• Lean.Parser.timeCmd = Lean.ParserDescr.node `Lean.Parser.timeCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#time ") (Lean.ParserDescr.cat `command 0))

def Lean.Parser.discrTreeKeyCmd : ParserDescr

#discr_tree_key t prints the discrimination tree keys for a term t (or, if it is a single identifier, the type of that constant). It uses the default configuration for generating keys.

For example,

#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)

#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _

#discr_tree_simp_key is similar to #discr_tree_key, but treats the underlying type as one of a simp lemma, i.e. transforms it into an equality and produces the key of the left-hand side.

Equations

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

def Lean.Parser.discrTreeSimpKeyCmd : ParserDescr

#discr_tree_key t prints the discrimination tree keys for a term t (or, if it is a single identifier, the type of that constant). It uses the default configuration for generating keys.

For example,

#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)

#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _

#discr_tree_simp_key is similar to #discr_tree_key, but treats the underlying type as one of a simp lemma, i.e. transforms it into an equality and produces the key of the left-hand side.

Equations

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

def Lean.Parser.commandSeal__ : ParserDescr

The seal foo command ensures that the definition of foo is sealed, meaning it is marked as [irreducible]. This command is particularly useful in contexts where you want to prevent the reduction of foo in proofs.

In terms of functionality, seal foo is equivalent to attribute [local irreducible] foo. This attribute specifies that foo should be treated as irreducible only within the local scope, which helps in maintaining the desired abstraction level without affecting global settings.

Equations

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

def Lean.Parser.commandUnseal__ : ParserDescr

The unseal foo command ensures that the definition of foo is unsealed, meaning it is marked as [semireducible], the default reducibility setting. This command is useful when you need to allow some level of reduction of foo in proofs.

Functionally, unseal foo is equivalent to attribute [local semireducible] foo. Applying this attribute makes foo semireducible only within the local scope.

Equations

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