doc-next-gen

Init.Notation

Module docstring

{"DSL for specifying parser precedences and priorities ","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. ","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. "}

Lean.Parser.Category structure
Full source 
/--
Auxiliary type used to represent syntax categories. We mainly use auxiliary
definitions with this type to attach doc strings to syntax categories.
-/
structure Parser.Category
Parser Category Structure
Informal description
The structure `Lean.Parser.Category` is an auxiliary type used to represent syntax categories in Lean's parser system. It serves as a container for attaching documentation to different syntax categories (such as commands or terms) within the parser framework.
Lean.Parser.Category.command definition
: Category
Full source 
/-- `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. -/
def command : Category := {}
Command syntax category
Informal description
The syntax category `command` represents the built-in category for top-level commands in Lean. A command is an instruction that can appear at the top level of a Lean file, such as definitions (`def foo := 1`), namespace declarations (`namespace Foo`), or variable declarations (`variable (x : Nat)`). Commands typically modify the environment by adding new declarations or changing the scope of subsequent commands.
Lean.Parser.Category.term definition
: Category
Full source 
/-- `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 `Expr`s depending on the context. -/
def term : Category := {}
Term Syntax Category
Informal description
The syntax category `term` represents the built-in category for terms in Lean's type theory. A term is an expression such as `2 + 2`. Unlike `Expr`, which is the result of elaboration, `term` is a syntactic construct that can elaborate to different `Expr` values depending on the context (e.g., `by simp` elaborates differently in different contexts).
Lean.Parser.Category.tactic definition
: Category
Full source 
/-- `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
```
-/
def tactic : Category := {}
Tactic syntax category
Informal description
The syntax category `tactic` represents the built-in category for tactics in Lean. Tactics are programs that appear after the keyword `by` in proofs and are used to construct terms of the expected type by manipulating the proof context (the available hypotheses and the goal type). For example, the `simp` tactic is used in `example : 2 + 2 = 4 := by simp` to simplify the expression to a proof of the equality.
Lean.Parser.Category.doElem definition
: Category
Full source 
/-- `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 `doElem`s. -/
def doElem : Category := {}
`do` block element syntax category
Informal description
The syntax category `doElem` represents elements that can appear within a `do` block in Lean's monadic notation. Examples include statements like `let x ← e` and other monadic operations.
Lean.Parser.Category.structInstFieldDecl definition
: Category
Full source 
/-- `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. -/
def structInstFieldDecl : Category := {}
Structure instance field declaration syntax category
Informal description
The syntax category `structInstFieldDecl` represents field declarations in structure instance notation. It includes the syntax for specifying values for fields when constructing instances of structures, such as the `:= 1` and pattern matching expressions in `{ x := 1, f | 0 => 0 | n + 1 => n }`.
Lean.Parser.Category.level definition
: Category
Full source 
/-- `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. -/
def level : Category := {}
Universe level syntax category
Informal description
The syntax category `level` represents universe levels in Lean, such as the `u` in `Sort u`. It supports expressions involving `max`, `imax`, addition with constants, and variables.
Lean.Parser.Category.attr definition
: Category
Full source 
/-- `attr` is a builtin syntax category for attributes.
Declarations can be annotated with attributes using the `@[...]` notation. -/
def attr : Category := {}
Attribute syntax category
Informal description
The syntax category `attr` represents attributes in Lean, which are annotations that can be attached to declarations using the `@[...]` notation. Attributes provide metadata or modify the behavior of declarations in various ways.
Lean.Parser.Category.stx definition
: Category
Full source 
/-- `stx` is a builtin syntax category for syntax. This is the abbreviated
parser notation used inside `syntax` and `macro` declarations. -/
def stx : Category := {}
Syntax category for parser notation
Informal description
The syntax category `stx` represents the built-in syntax category in Lean, which is used for abbreviated parser notation within `syntax` and `macro` declarations. It provides a way to define and manipulate syntax elements in Lean's parser system.
Lean.Parser.Category.prio definition
: Category
Full source 
/-- `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. -/
def prio : Category := {}
Priority Syntax Category
Informal description
The syntax category `prio` is used to define and manipulate priority levels in Lean's attribute system. Priorities are numerical values where higher numbers indicate higher precedence, influencing the order in which instances are considered during typeclass resolution. The category supports literal numbers (e.g., `37`) as well as relative levels (`low`, `mid`, `high`) and arithmetic operations (addition and subtraction) for adjusting priorities.
Lean.Parser.Category.prec definition
: Category
Full source 
/-- `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. -/
def prec : Category := {}
Precedence syntax category
Informal description
The syntax category `prec` is used to define and manipulate precedence levels in Lean's parser system. A precedence is a numerical value that determines how tightly a piece of syntax binds. For example, in the expression `1 + 2 * 3`, the multiplication `*` has a higher precedence than the addition `+`, causing the expression to be parsed as `1 + (2 * 3)`. Precedences can be specified using literal numbers (e.g., `37`) or special named levels: - `arg`: the precedence of function arguments - `max`: the highest precedence used in term parsers (not the maximum possible value) - `lead`: the precedence of terms not intended to be used as arguments Additionally, precedences can be adjusted using arithmetic operations like addition and subtraction (e.g., `max + 1` or `max - 1`).
Lean.Parser.Syntax.subPrio definition
: Lean.TrailingParserDescr✝
Full source 
/-- Subtraction of priorities. This is normally used only for offsetting, e.g. `default - 1`. -/
syntax:65 (name := subPrio) prio " - " prio:66 : prio
Subtraction of parser priorities
Informal description
The syntax rule for subtracting parser priorities, typically used for offsetting, such as in expressions like `default - 1`. The syntax has a precedence level of 65, and the right-hand side of the subtraction has a precedence level of 66.
Lean.instCoeOutTSyntaxSyntax instance
: CoeOut (TSyntax ks) Syntax
Full source 
instance : CoeOut (TSyntax ks) Syntax where
  coe stx := stx.raw
Canonical View of Syntax Terms as Syntax
Informal description
For any syntax term `TSyntax ks`, there is a canonical way to view it as a `Syntax` term.
Lean.instCoeSyntaxNodeKindSyntaxNodeKinds instance
: Coe SyntaxNodeKind SyntaxNodeKinds
Full source 
instance : Coe SyntaxNodeKind SyntaxNodeKinds where
  coe k := List.cons k List.nil
Coercion from Syntax Node Kind to Syntax Node Kinds
Informal description
There is a canonical coercion from a syntax node kind to a set of syntax node kinds in the Lean parser system.
precMax definition
: Lean.ParserDescr✝
Full source 
macromacro "max"  : prec => `(prec| 1024)
Maximum parser precedence
Informal description
The constant `precMax` represents the maximum precedence value (1024) used in term parsers, particularly for terms appearing in function position (such as identifiers, parenthesized expressions, etc.).
precArg definition
: Lean.ParserDescr✝
Full source 
macromacro "arg"  : prec => `(prec| 1023)
Precedence level for application arguments
Informal description
The precedence level `1023` is used for application arguments (such as `do`, `by`, etc.) in parser specifications.
precLead definition
: Lean.ParserDescr✝
Full source 
macromacro "lead" : prec => `(prec| 1022)
Lead precedence level
Informal description
The precedence level `lead` is defined as 1022, intended for terms that are not meant to be used as arguments (such as `let`, `have`, etc.).
prec(_) definition
: Lean.ParserDescr✝
Full source 
macromacro "(" p:prec ")" : prec => return p
Parenthesized precedence expression
Informal description
The `prec(_)` macro is used to group precedence expressions in parentheses, allowing for explicit control over parsing precedence in Lean's DSL for parser specifications.
precMin definition
: Lean.ParserDescr✝
Full source 
macromacro "min"  : prec => `(prec| 10)
Minimum parser precedence
Informal description
The minimum precedence level used in term parsers, set to 10.
precMin1 definition
: Lean.ParserDescr✝
Full source 
macromacro "min1" : prec => `(prec| 11)
Parser precedence level min+1
Informal description
The parser precedence level `min1` is defined to be `11`, representing a minimal precedence level plus one increment.
termMax_prec definition
: Lean.ParserDescr✝
Full source 
macromacro "max_prec" : term => `(1024)
Maximum parser precedence value
Informal description
The term `max_prec` represents the maximum precedence value (1024) used in parser specifications. It is equivalent to evaluating `eval_prec max` where `eval_prec` is defined in `Meta.lean`. This definition is primarily used to circumvent bootstrapping issues in the system.
prioDefault definition
: Lean.ParserDescr✝
Full source 
macromacro "default" : prio => `(prio| 1000)
Default parser priority
Informal description
The default priority value `1000` is assigned when no explicit priority is specified for a parser.
prioLow definition
: Lean.ParserDescr✝
Full source 
macromacro "low"     : prio => `(prio| 100)
Low parser priority constant
Informal description
The constant `low` is defined as `100` and represents a standardized low priority level for parser operations, intended to be lower than the default priority.
prioMid definition
: Lean.ParserDescr✝
Full source 
macromacro "mid"     : prio => `(prio| 500)
Medium priority level (500)
Informal description
The predefined medium priority level `mid` is set to 500. This priority is lower than the default priority and higher than the low priority.
prioHigh definition
: Lean.ParserDescr✝
Full source 
macromacro "high"    : prio => `(prio| 10000)
High priority value
Informal description
The standardized "high" priority value `high` is defined as `10000`, intended for cases where a higher priority than the default is needed.
prio(_) definition
: Lean.ParserDescr✝
Full source 
macromacro "(" p:prio ")" : prio => return p
Parentheses for priority grouping
Informal description
The `prio(_)` macro is used to group priority expressions in parentheses when specifying parser precedences and priorities. It simply returns the enclosed priority expression `p` unchanged.
stx_+ definition
: Lean.TrailingParserDescr✝
Full source 
/--
`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.
-/
syntax:arg stx:max "+" : stx
One or more occurrences parser (`p+`)
Informal description
The parser `p+` is a shorthand for `many1(p)`, which applies parser `p` one or more times and produces a `nullNode` containing an array of the parsed results. This parser has arity 1. If `p` has arity greater than 1, the items generated by the parser are automatically grouped.
stx_* definition
: Lean.TrailingParserDescr✝
Full source 
/--
`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.
-/
syntax:arg stx:max "*" : stx
Kleene star parser notation
Informal description
The syntax `p*` is a shorthand notation for `many(p)`, which applies parser `p` zero or more times and produces a `nullNode` containing an array of the parsed results. This parser has arity 1. If `p` has arity greater than 1, it is automatically grouped in the items generated by the parser.
stx_? definition
: Lean.TrailingParserDescr✝
Full source 
/--
`(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.
-/
syntax:arg stx:max "?" : stx
Optional parser notation (`p?`)
Informal description
The syntax `p?` is a shorthand for `optional(p)`, which applies parser `p` zero or one times and produces a `nullNode` containing an array of the parsed results. This parser has arity 1. If `p` has arity greater than 1, the node will have either 0 or n children, but if `p` has arity 0, the result will be ambiguous. Note that because `?` is an identifier character, `ident?` will not work as intended; one must write either `ident ?` or `(ident)?` for it to parse as the `?` combinator applied to the `ident` parser.
stx_<|>_ definition
: Lean.TrailingParserDescr✝
Full source 
/--
`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`.
-/
syntax:2 stx:2 " <|> " stx:1 : stx
Alternative parser combinator `<|>`
Informal description
The syntax `p₁ <|> p₂` is a shorthand for the parser combinator `orelse(p₁, p₂)`, which attempts to parse either `p₁` or `p₂`. If `p₁` consumes at least one token (even if it ultimately fails), `p₂` will not be attempted. The parsers `p₁` and `p₂` should differ in their first token to ensure predictable behavior. If the inner parser does not produce exactly one syntax node, it is automatically wrapped in a `group` node to ensure the result has arity 1. The `<|>` combinator itself does not generate a node, so the parsers `p₁` and `p₂` should use distinct node kinds for proper reconstruction of the parse.
stx_,* definition
: Lean.TrailingParserDescr✝
Full source 
macromacro:arg x:stx:max ",*"   : stx => `(stx| sepBy($x, ",", ", "))
Zero or more comma-separated occurrences parser
Informal description
The notation `p,*` is a shorthand for parsing zero or more occurrences of `p` separated by commas, producing a structured syntax node containing the parsed elements in a separated array. It is equivalent to the patterns: empty, `p`, `p,p`, `p,p,p`, etc.
stx_,+ definition
: Lean.TrailingParserDescr✝
Full source 
macromacro:arg x:stx:max ",+"   : stx => `(stx| sepBy1($x, ",", ", "))
One or more comma-separated parsers
Informal description
The parser `p,+` is a shorthand notation that parses one or more occurrences of a parser `p` separated by commas (`,`). It produces a syntax tree node containing an array of the parsed results with the separators. The parser has arity 1 and automatically groups its component parser if necessary.
stx_,*,? definition
: Lean.TrailingParserDescr✝
Full source 
macromacro:arg x:stx:max ",*,?" : stx => `(stx| sepBy($x, ",", ", ", allowTrailingSep))
Comma-separated list parser with optional trailing comma
Informal description
The parser `p,*,?` is a shorthand notation for parsing zero or more occurrences of `p` separated by commas, allowing for an optional trailing comma. It produces a structured output containing the parsed elements in an array format.
stx_,+,? definition
: Lean.TrailingParserDescr✝
Full source 
macromacro:arg x:stx:max ",+,?" : stx => `(stx| sepBy1($x, ",", ", ", allowTrailingSep))
Comma-separated list parser with optional trailing comma
Informal description
The parser `p,+,?` is a shorthand notation for parsing one or more occurrences of parser `p` separated by commas, with an optional trailing comma. It produces a syntax tree node containing an array of the parsed results, including the separators. This parser automatically groups its component parser if needed.
rawNatLit definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := rawNatLit) "nat_lit " num : term
Raw numeric literal constructor
Informal description
The `nat_lit` macro constructs raw numeric literals, corresponding to the `Expr.lit (.natVal n)` constructor in the `Expr` data type. Normally, numerals like `37` are parsed as applications of `OfNat.ofNat` to cast them into the target type, even when the target type is `Nat`. However, `nat_lit` allows direct reference to the raw numeral, which is particularly useful when proving properties about the `ofNat` function.
term_∘_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:90 " ∘ "  => Function.comp
Function composition notation
Informal description
The infix notation `∘` with right associativity and precedence level 90 represents function composition, where `f ∘ g` denotes the composition of functions `f` and `g`.
term_×_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:35 " × "  => Prod
Product type notation
Informal description
The infix operator `×` with right associativity and precedence level 35 is defined as a notation for the product type constructor `Prod`.
term_×'_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:35 " ×' " => PProd
Parallel product notation (`×'`)
Informal description
The notation `×'` is defined as an infix right-associative operator with precedence 35, representing the `PProd` (parallel product) operation.
term_∣_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50  " ∣ " => Dvd.dvd
Divisibility notation
Informal description
The infix notation `∣` with precedence 50 represents the divisibility relation `Dvd.dvd`, where `a ∣ b` means "$a$ divides $b$".
term_|||_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:55 " ||| " => HOr.hOr
Horizontal composition operator `|||`
Informal description
The infix operator `|||` with precedence level 55 represents the horizontal composition operation `HOr.hOr` in Lean's parser DSL. It is used to combine parsers in sequence, where the left parser is applied first, followed by the right parser.
term_^^^_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:58 " ^^^ " => HXor.hXor
Bitwise XOR operator
Informal description
The infix operator `^^^` with left associativity and precedence level 58 represents the bitwise XOR (exclusive OR) operation between two values. It is defined using the `HXor.hXor` function.
term_&&&_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:60 " &&& " => HAnd.hAnd
Logical "and" operator (`&&&`)
Informal description
The infix operator `&&&` with left associativity and precedence level 60 represents the logical "and" operation (`HAnd.hAnd`).
term_+_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:65 " + "   => HAdd.hAdd
Addition operator with precedence 65
Informal description
The infix left-associative operator `+` with precedence level 65, representing addition via the `HAdd.hAdd` function.
term_-_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:65 " - "   => HSub.hSub
Subtraction operator
Informal description
The infix operator `-` with left associativity and precedence level 65, representing subtraction or the `HSub.hSub` operation.
term_*_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:70 " * "   => HMul.hMul
Multiplication operator definition
Informal description
The infix operator `*` with left associativity and precedence level 70, representing multiplication via the `HMul.hMul` function.
term_/_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:70 " / "   => HDiv.hDiv
Division operator with precedence 70
Informal description
The infix operator `/` with left associativity and precedence level 70, representing the division operation `HDiv.hDiv`.
term_%_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:70 " % "   => HMod.hMod
Modulo operator notation
Informal description
The infix operator `%` with left associativity and precedence level 70 is defined as notation for the `HMod.hMod` operation (heterogeneous modulo operation).
term_<<<_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:75 " <<< " => HShiftLeft.hShiftLeft
Left shift operator `<<<`
Informal description
The infix operator `<<<` with precedence 75 represents the left shift operation `HShiftLeft.hShiftLeft`, which shifts the bits of its first operand to the left by the number of positions specified by its second operand.
term_>>>_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:75 " >>> " => HShiftRight.hShiftRight
Right shift operator `>>>`
Informal description
The infix operator `>>>` with precedence level 75 represents the right shift operation `HShiftRight.hShiftRight` between two operands.
term_^_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:80 " ^ "   => HPow.hPow
Power notation `^`
Informal description
The notation `^` is defined as an infix right-associative operator with precedence 80, representing the power operation `HPow.hPow`.
term_++_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:65 " ++ "  => HAppend.hAppend
Append operator (`++`)
Informal description
The infix operator `++` with left associativity and precedence level 65 represents the `HAppend.hAppend` operation, which is used for appending two structures (like lists or strings) together.
term-_ definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc] prefix:75 "-"    => Neg.neg
Unary negation operator
Informal description
The prefix operator `-` with precedence 75 represents the unary negation operation, mapping an element to its additive inverse.
term_<=_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " <= " => LE.le
Less-than-or-equal-to notation
Informal description
The infix notation `<=` represents the less-than-or-equal-to relation `LE.le`, with a precedence level of 50.
term_≤_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " ≤ "  => LE.le
Parser for the less-than-or-equal-to relation (≤)
Informal description
The parser definition for the binary relation "less than or equal to" symbol `≤`, with infix notation precedence level 50. This enables the symbol to be used in Lean expressions with the specified precedence.
term_<_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " < "  => LT.lt
Less than notation
Informal description
The infix notation `a < b` represents the "less than" relation between elements `a` and `b`, implemented via the `LT.lt` operation.
term_>=_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " >= " => GE.ge
Greater than or equal to notation
Informal description
The infix notation `>=` is defined as an alias for the greater than or equal to operation `GE.ge`.
term_≥_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " ≥ "  => GE.ge
Greater than or equal to operator parser
Informal description
The parser definition for the binary relation "greater than or equal to" (≥) with precedence 50.
term_>_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " > "  => GT.gt
Greater-than notation
Informal description
The infix notation `>` is defined as the greater-than relation `GT.gt`, with a precedence level of 50.
term_=_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " = "  => Eq
Equality notation
Informal description
The infix notation `=` with precedence 50 represents the equality relation between two terms.
term_==_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infix:50 " == " => BEq.beq
Boolean equality notation
Informal description
The infix notation `==` with precedence 50, which stands for the boolean equality operation `BEq.beq`.
term_/\_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:35 " /\\ " => And
Logical conjunction operator
Informal description
The infix operator `∧` (logical and) with right associativity and precedence level 35.
term_∧_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:35 " ∧ "   => And
Logical AND notation
Informal description
The infix notation `∧` with right associativity and precedence level 35 represents the logical AND operation.
term_\/_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:30 " \\/ " => Or
Logical OR notation
Informal description
The infix notation `\/` with right associativity and precedence level 30 represents the logical disjunction (OR) operation.
term_∨_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:30 " ∨  "  => Or
Disjunction operator parser rule
Informal description
The parser rule for the logical disjunction operator `∨` with right associativity and precedence level 30.
term¬_ definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc] notation:max "¬" p:40 => Not p
Logical negation notation
Informal description
The notation `¬p` represents the logical negation of the proposition `p`, with a precedence level of 40.
term_&&_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:35 " && " => and
Logical AND operator (&&) with precedence 35
Informal description
The infix operator `&&` with left associativity and precedence level 35, representing logical conjunction (and).
term_||_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:30 " || " => or
Logical OR operator with precedence 30
Informal description
The infix operator `||` with left associativity and precedence level 30 represents the logical disjunction (OR) operation.
term!_ definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc] notation:max "!" b:40 => not b
Logical negation notation
Informal description
The notation `!b` represents the logical negation of the boolean expression `b`, with precedence level 40.
term_∈_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] notation:50 a:50 " ∈ " b:50 => Membership.mem b a
Membership notation
Informal description
The notation `a ∈ b` is defined as `Membership.mem b a`, where `a` is an element and `b` is a set or type. This notation is used to denote the membership relation, i.e., that `a` is an element of `b`.
term_::_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:67 " :: " => List.cons
List cons notation
Informal description
The notation `a :: b` represents the list constructor, where `a` is prepended to the list `b`. This is equivalent to `List.cons a b`.
term_<$>_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixr:100 " <$> " => Functor.map
Functor map operator (`<$>`)
Informal description
The infix operator `<$>` with precedence 100 is defined as an alias for the `Functor.map` operation, which applies a function to the value inside a functor.
term_>>=_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc] infixl:55  " >>= " => Bind.bind
Monadic bind operator
Informal description
The infix operator `>>=` with precedence level 55 represents the bind operation in a monadic context, typically used for sequencing monadic computations. It is left-associative (indicated by `infixl`).
term_<|>_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc HOrElse.hOrElse]   syntax:20 term:21 " <|> " term:20 : term
Parser alternative combinator (`<|>`)
Informal description
The syntax `term₁ <|> term₂` represents a parser combinator that tries to parse `term₁`, and if that fails, it attempts to parse `term₂` instead. This is known as the "alternative" or "choice" combinator in parser combinator libraries.
term_>>_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc HAndThen.hAndThen] syntax:60 term:61 " >> " term:60 : term
Parser sequencing operator `>>`
Informal description
The syntax rule `term_>>_` defines a parser for the `>>` operator in Lean, which sequences two parsers, discarding the result of the first and returning the result of the second. The precedence level is set to 60 for both the left and right operands.
term_<*>_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc Seq.seq]           syntax:60 term:60 " <*> " term:61 : term
Applicative sequencing parser combinator (`<*>`)
Informal description
The syntax `term₁ <*> term₂` represents a parser combinator that applies the parser `term₁` to produce a function, then applies the parser `term₂` to produce an argument, and finally applies the function to the argument. This is known as the "applicative sequencing" combinator in parser combinator libraries, with precedence levels 60 for the left operand and 61 for the right operand.
term_<*_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc SeqLeft.seqLeft]   syntax:60 term:60 " <* " term:61 : term
Parser sequencing operator `<*` (keep left)
Informal description
The syntax rule `term_<*_` defines a parser for the `<*` operator in Lean, which sequences two parsers, returning the result of the first and discarding the result of the second. The precedence level is set to 60 for the left operand and 61 for the right operand.
term_*>_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc SeqRight.seqRight] syntax:60 term:60 " *> " term:61 : term
Sequence right parser combinator (`*>`)
Informal description
The syntax `term₁ *> term₂` represents a parser combinator that first applies the parser `term₁`, then applies the parser `term₂`, and returns the result of `term₂` while discarding the result of `term₁`. This is known as the "sequence right" combinator in parser combinator libraries, with precedence levels 60 for the left operand and 61 for the right operand.
Lean.binderIdent definition
: Lean.ParserDescr✝
Full source 
/--
`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.
-/
syntax binderIdent := ident <|> hole
Binder identifier parser
Informal description
The parser `binderIdent` matches either an identifier or an underscore `_`. It is used in binding contexts where an underscore indicates that the bound value should remain unnamed and inaccessible.
termDepIfThenElse definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc dite] syntax (name := termDepIfThenElse)
  ppRealGroup(ppRealFill(ppIndent("if " Lean.binderIdent " : " term " then") ppSpace term)
    ppDedent(ppSpace) ppRealFill("else " term)) : term
Dependent if-then-else term syntax parser
Informal description
The parser descriptor for the dependent `if-then-else` term syntax in Lean, which allows conditional expressions of the form `if h : c then t else e`, where `h` is a binder for the proof of the condition `c`, `t` is the term to evaluate if `c` is true, and `e` is the term to evaluate if `c` is false.
termIfThenElse definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc ite] syntax (name := termIfThenElse)
  ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace term)
    ppDedent(ppSpace) ppRealFill("else " term)) : term
`if-then-else` term syntax parser
Informal description
The parser descriptor for the `if-then-else` term syntax in Lean, which allows conditional expressions of the form `if c then t else e`, where `c` is the condition, `t` is the term to evaluate if `c` is true, and `e` is the term to evaluate if `c` is false.
termIfLet definition
: Lean.ParserDescr✝
Full source 
/--
`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.
-/
syntax (name := termIfLet)
  ppRealGroup(ppRealFill(ppIndent("if " "let " term " := " term " then") ppSpace term)
    ppDedent(ppSpace) ppRealFill("else " term)) : term
Pattern matching if-let syntax
Informal description
The syntax `if let pat := d then t else e` is a shorthand for pattern matching `d` against `pat`. If the pattern matches, the bindings are available in `t` and `t` is evaluated; otherwise, `e` is evaluated.
boolIfThenElse definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc cond] syntax (name := boolIfThenElse)
  ppRealGroup(ppRealFill(ppIndent("bif " term " then") ppSpace term)
    ppDedent(ppSpace) ppRealFill("else " term)) : term
Boolean if-then-else syntax
Informal description
The syntax `bif c then t else e` is a conditional expression that evaluates to `t` if the boolean condition `c` is true, and to `e` otherwise. This is similar to the standard `if-then-else` construct but is specifically designed for boolean conditions.
term_<|_ definition
: Lean.TrailingParserDescr✝
Full source 
/--
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`.
-/
syntax:min term " <| " term:min : term
Low-precedence application operator `<|`
Informal description
The operator `<|` is a Haskell-like pipe operator where `f <| x` is equivalent to `f x`, but with lower parsing precedence for `x`. This means that nested applications like `f <| g <| x` are interpreted as `f (g x)` instead of `(f g) x`.
term_$__ definition
: Lean.TrailingParserDescr✝
Full source 
/--
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`.
-/
-- Note that we have a whitespace after `$` to avoid an ambiguity with antiquotations.
syntax:min term atomic(" $" ws) term:min : term
Low-precedence function application operator
Informal description
The operator `$` provides an alternative syntax for function application with lower precedence parsing. Specifically, `f $ x` is equivalent to `f x`, but `x` is parsed with lower precedence, so that `f $ g $ x` is interpreted as `f (g x)` instead of `(f g) x`.
termWithout_expected_type_ definition
: Lean.ParserDescr✝
Full source 
macromacro "without_expected_type " x:term : term => `(let aux := $x; aux)
Elaboration without expected type
Informal description
The macro `without_expected_type t` instructs the Lean proof assistant to elaborate the term `t` without requiring an expected type. This is useful for terms like `match` expressions and structure constructors `⟨...⟩` that normally delay their elaboration until their expected type is known. Note that this macro may not be effective for such cases.
Lean.byElab definition
: Lean.ParserDescr✝
Full source 
/--
* 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.
-/
syntax (name := byElab) "by_elab " doSeq : term
Expression elaboration via `TermElabM` monad
Informal description
The `by_elab` expression allows running a sequence of commands (`doSeq`) in the `TermElabM Expr` monad to synthesize an expression. It can optionally receive the expected type as an `Option Expr` parameter.
Lean.rawStx.quot definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
declare_syntax_cat rawStx
Raw syntax tree quotation parser
Informal description
The parser descriptor for raw syntax tree quotations, which allows carrying unprocessed syntax trees between macros. Any content within these quotations is printed exactly as provided by the pretty printer. The only accepted parser for this category is an antiquotation.
Lean.Parser.Category.rawStx definition
: Lean.Parser.Category✝
Full source 
/--
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.
-/
declare_syntax_cat rawStx
Raw Syntax Tree Category
Informal description
The category `rawStx` is used to carry unprocessed syntax trees between macros in Lean's parsing system. Any content within this category is printed verbatim by the pretty printer, and the only parser accepted for this category is an antiquotation.
Lean.instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStr1Nil instance
: Coe Syntax (TSyntax `rawStx)
Full source 
instance : Coe Syntax (TSyntax `rawStx) where
  coe stx := ⟨stx⟩
Coercion from Raw Syntax to Typed Syntax Trees
Informal description
There exists a coercion from raw syntax to typed syntax trees of kind `rawStx`.
Lean.withAnnotateTerm definition
: Lean.ParserDescr✝
Full source 
/-- `with_annotate_term stx e` annotates the lexical range of `stx : Syntax` with term info for `e`. -/
scoped syntax (name := withAnnotateTerm) "with_annotate_term " rawStx ppSpace term : term
Syntax annotation with term information
Informal description
The function `with_annotate_term` annotates the lexical range of a syntax object `stx` with term information for the expression `e`. This is used to associate term information with specific parts of the syntax during parsing.
Lean.deprecated definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
    (" (" &"since" " := " str ")")? : attr
Deprecation Attribute
Informal description
The attribute `@[deprecated]` marks a declaration as discouraged for use in new code and suggests migration away from it in existing code. It may be removed in future versions. - `@[deprecated myBetterDef]` indicates that `myBetterDef` is the recommended replacement. - `@[deprecated myBetterDef "use myBetterDef instead"]` allows specifying a custom deprecation message. - `@[deprecated (since := "2024-04-21")]` records the date when the deprecation was first applied.
Lean.Attr.coe definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := Attr.coe) "coe" : attr
Coe attribute for coercion display
Informal description
The `@[coe]` attribute marks a function (which should also be part of a coercion instance declaration `instance : Coe A B := ⟨myFn⟩`) to indicate that applications of this function should be displayed using the up-arrow notation `↑` when printing expressions.
Lean.command_code_action definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
Command Code Action Attribute
Informal description
The attribute `@[command_code_action]` marks a code action that can suggest or modify tactics when processing commands in Lean. - When applied to specific command syntax kinds (e.g., `@[command_code_action kind]`), it enables code actions that replace or modify those commands. - When applied without arguments (`@[command_code_action]`), it applies to all commands (though this should be used sparingly).
Lean.builtin_command_code_action definition
: Lean.ParserDescr✝
Full source 
/--
Builtin command code action. See `command_code_action`.
-/
syntax (name := builtin_command_code_action) "builtin_command_code_action" (ppSpace ident)* : attr
Built-in command code action attribute
Informal description
The attribute `builtin_command_code_action` is used to mark built-in command code actions in the Lean theorem prover. It allows specifying identifiers that represent built-in code actions for commands.
Lean.includeStr definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := includeStr) "include_str " term : term
File content inclusion as string
Informal description
The `include_str` command reads the contents of a file specified by a path relative to the directory containing the current Lean file and returns it as a string literal. If the file cannot be read, the elaboration fails.
Lean.runMeta definition
: Lean.ParserDescr✝
Full source 
/--
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`.)
-/
syntax (name := runMeta) "run_meta " doSeq : command
Meta-programming execution command
Informal description
The `run_meta` command executes a sequence of operations in the `MetaM` monad, which is used for meta-programming in Lean. It is equivalent to evaluating `#eval show MetaM Unit from do discard doSeq` and serves as a synonym for `run_elab` since `MetaM` can be lifted to `TermElabM`.
Lean.reduceCmd definition
: Lean.ParserDescr✝
Full source 
/--
`#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.
-/
syntax (name := reduceCmd) "#reduce " (atomic("(" &"proofs" " := " &"true" ")"))? (atomic("(" &"types" " := " &"true" ")"))? term : command
Expression Reduction Command
Informal description
The `#reduce` command reduces a given expression to its normal form by applying reduction rules until no further reduction is possible. By default, proofs and types within the expression are not reduced, but this behavior can be modified using the optional arguments `(proofs := true)` and `(types := true)` to enable reduction of proofs and types, respectively. Note that propositions are types in Lean. **Warning:** This operation can be computationally expensive, especially for complex expressions. For simple evaluation or execution of expressions, consider using `#eval` instead.
Lean.guardMsgsFilter definition
: Lean.ParserDescr✝
Full source 
/--
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture messages with the given severity level.
- `all`: capture all messages (the default).
- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
- `drop all`: drop every message.
These filters are processed in left-to-right order.
-/
syntax guardMsgsFilter := &"drop"? guardMsgsFilterSeverity
Message filter specification for `#guard_msgs`
Informal description
A message filter specification for the `#guard_msgs` command, which can be used to selectively capture or drop messages based on their severity level. The filter can be: - `info`, `warning`, `error`: capture messages with the specified severity level - `all`: capture all messages (default behavior) - `drop info`, `drop warning`, `drop error`: drop messages with the specified severity level - `drop all`: drop all messages Filters are processed in left-to-right order.
Lean.guardMsgsWhitespaceArg definition
: Lean.ParserDescr✝
Full source 
syntax guardMsgsWhitespaceArg := &"exact" <|> &"normalized" <|> &"lax"
Whitespace argument validator for message guarding
Informal description
The parser syntax definition for whitespace argument validation in message guarding, which accepts one of three possible string literals: "exact", "normalized", or "lax".
Lean.guardMsgsWhitespace definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax guardMsgsWhitespace := &"whitespace" " := " guardMsgsWhitespaceArg
Whitespace handling for message guarding
Informal description
The syntax definition for specifying whitespace handling in message guarding, which accepts one of three modes: - `exact`: requires an exact whitespace match. - `normalized`: converts all newline characters to a single space before matching (default behavior). - `lax`: collapses all whitespace to a single space before matching. In all cases, leading and trailing whitespace is trimmed before matching.
Lean.guardMsgsOrderingArg definition
: Lean.ParserDescr✝
Full source 
syntax guardMsgsOrderingArg := &"exact" <|> &"sorted"
Ordering argument validator for message guarding
Informal description
The parser syntax definition for ordering argument validation in message guarding, which accepts one of two possible string literals: "exact" or "sorted".
Lean.guardMsgsOrdering definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax guardMsgsOrdering := &"ordering" " := " guardMsgsOrderingArg
Message ordering specification for `#guard_msgs`
Informal description
The syntax definition for specifying message ordering in the `#guard_msgs` command, which accepts either `ordering := exact` (default, preserving original message order) or `ordering := sorted` (sorting messages lexicographically for non-deterministic outputs).
Lean.guardMsgsSpec definition
: Lean.ParserDescr✝
Full source 
syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
Message Guard Specification Syntax
Informal description
The syntax definition for the specification of the `#guard_msgs` command, which consists of a comma-separated list of message guard specification elements enclosed in parentheses.
Lean.guardMsgsCmd definition
: Lean.ParserDescr✝
Full source 
/--
`/-- ... -/ #guard_msgs in cmd` captures the messages generated by the command `cmd`
and checks that they match the contents of the docstring.

Basic example:
```lean
/--
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:
```lean
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
```
or only errors
```lean
#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
```lean
#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 `(all, whitespace := normalized, ordering := exact)`.

Message filters (processed in left-to-right order):
- `info`, `warning`, `error`: capture messages with the given severity level.
- `all`: capture all messages (the default).
- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
- `drop all`: drop every message.

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.
-/
syntax (name := guardMsgsCmd)
  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
Message Guard Command
Informal description
The command `#guard_msgs` captures and checks the messages (info, warnings, errors) generated by a given command against the contents of its docstring. It supports various configurations for message filtering, whitespace handling, and message ordering. By default, it captures all messages, normalizes whitespace, and checks for exact ordering. Additional options allow selecting specific message types, dropping others, and adjusting whitespace and ordering handling.
Lean.setPremiseSelectorCmd definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax (name := setPremiseSelectorCmd)
  "set_premise_selector" term : command
Premise selection engine specification command
Informal description
The command `set_premise_selector` specifies a premise selection engine for Lean. Note that Lean does not include a default premise selection engine, so this command is only useful when used with an external package that provides one.
Lean.Parser.checkTactic definition
: Lean.ParserDescr✝
Full source 
/--
`#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`.
-/
syntax (name := checkTactic) "#check_tactic " term "~>" term "by" tactic : command
Tactic verification command
Informal description
The command `#check_tactic t ~> r by commands` executes the tactic sequence `commands` on a goal containing the term `t` and verifies whether the resulting expression reduces to `r`.
Lean.Parser.timeCmd definition
: Lean.ParserDescr✝
Full source 
/--
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
```
-/
syntax (name := timeCmd) "#time " command : command
Time Command
Informal description
The `#time` command measures and prints the time (in milliseconds) taken to elaborate a given Lean command. Example usage: ``` #time example : (List.range 500).length = 500 := rfl ```
Lean.Parser.discrTreeKeyCmd definition
: Lean.ParserDescr✝
Full source 
/--
`#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.
-/
syntax (name := discrTreeKeyCmd) "#discr_tree_key " term : command
Discrimination Tree Key Command
Informal description
The command `#discr_tree_key t` generates and displays the discrimination tree keys for a given term `t`. If `t` is a single identifier, it uses the type of that constant. The keys are generated using the default configuration. For example: - `#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))` produces keys like `bar _ (@OfNat.ofNat Nat _ _)`. - `#discr_tree_simp_key Nat.add_assoc` treats the term as a simp lemma, converts it to an equality, and generates keys for the left-hand side.
Lean.Parser.commandSeal__ definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax "seal " (ppSpace ident)+ : command
Seal command for making definitions irreducible
Informal description
The `seal` command marks a given definition as `[irreducible]` within the local scope, preventing its reduction in proofs. This is equivalent to applying the attribute `attribute [local irreducible]` to the definition.
Lean.Parser.commandUnseal__ definition
: Lean.ParserDescr✝
Full source 
/--
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.
-/
syntax "unseal " (ppSpace ident)+ : command
Unseal command for semireducible definitions
Informal description
The command `unseal foo` marks the definition of `foo` as semireducible, allowing some level of reduction of `foo` in proofs. This is equivalent to applying the attribute `[local semireducible] foo`, which makes `foo` semireducible only within the local scope.