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

## Instances For

`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.

## Instances For

`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.

## Instances For

`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
```

## Instances For

`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.

## Instances For

`attr`

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

notation.

## Instances For

`stx`

is a builtin syntax category for syntax. This is the abbreviated
parser notation used inside `syntax`

and `macro`

declarations.

## Instances For

`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.

## Instances For

`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 pr0ecedence than `+`

.
Higher numbers denote higher precedence.
In addition to literals like `37`

, there are some special named priorities:

`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.

## Instances For

DSL for specifying parser precedences and priorities

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

.

## Instances For

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

.

## Instances For

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

.

## Instances For

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

.

## Instances For

Maximum precedence used in term parsers, in particular for terms in
function position (`ident`

, `paren`

, ...)

## Instances For

Precedence used for application arguments (`do`

, `by`

, ...).

## Instances For

Precedence used for terms not supposed to be used as arguments (`let`

, `have`

, ...).

## Instances For

Parentheses are used for grouping precedence expressions.

## Instances For

`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.

## Instances For

The default priority `default = 1000`

, which is used when no priority is set.

## Instances For

The standardized "low" priority `low = 100`

, for things that should be lower than default priority.

## Instances For

The standardized "medium" priority `mid = 500`

. This is lower than `default`

, and higher than `low`

.

## Instances For

The standardized "high" priority `high = 10000`

, for things that should be higher than default priority.

## Instances For

Parentheses are used for grouping priority expressions.

## Instances For

`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.

## Instances For

`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.

## Instances For

`(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.

## Instances For

`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`

.

## Instances For

`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.

## Instances For

`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.

## Instances For

`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.

## Instances For

`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 | ...`

.

`nullNode`

containing a `SepArray`

with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.

## Instances For

`!p`

parses the negation of `p`

. That is, it fails if `p`

succeeds, and
otherwise parses nothing. It has arity 0.

## Instances For

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.

## Instances For

Function composition is the act of pipelining the result of one function, to the input of another, creating an entirely new function. Example:

```
#eval Function.comp List.reverse (List.drop 2) [3, 2, 4, 1]
-- [1, 4]
```

You can use the notation `f ∘ g`

as shorthand for `Function.comp f g`

.

```
#eval (List.reverse ∘ List.drop 2) [3, 2, 4, 1]
-- [1, 4]
```

A simpler way of thinking about it, is that `List.reverse ∘ List.drop 2`

is equivalent to `fun xs => List.reverse (List.drop 2 xs)`

,
the benefit is that the meaning of composition is obvious,
and the representation is compact.

## Instances For

Product type (aka pair). You can use `α × β`

as notation for `Prod α β`

.
Given `a : α`

and `b : β`

, `Prod.mk a b : Prod α β`

. You can use `(a, b)`

as notation for `Prod.mk a b`

. Moreover, `(a, b, c)`

is notation for
`Prod.mk a (Prod.mk b c)`

.
Given `p : Prod α β`

, `p.1 : α`

and `p.2 : β`

. They are short for `Prod.fst p`

and `Prod.snd p`

respectively. You can also write `p.fst`

and `p.snd`

.
For more information: Constructors with Arguments

## Instances For

`a ||| b`

computes the bitwise OR of `a`

and `b`

.
The meaning of this notation is type-dependent.

## Instances For

`a ^^^ b`

computes the bitwise XOR of `a`

and `b`

.
The meaning of this notation is type-dependent.

## Instances For

`a &&& b`

computes the bitwise AND of `a`

and `b`

.
The meaning of this notation is type-dependent.

## Instances For

`a + b`

computes the sum of `a`

and `b`

.
The meaning of this notation is type-dependent.

## Instances For

`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`

.

## Instances For

`a * b`

computes the product of `a`

and `b`

.
The meaning of this notation is type-dependent.

## Instances For

`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`

and`Int`

,`a / b`

rounds toward 0. - For
`Float`

,`a / 0`

follows the IEEE 754 semantics for division, usually resulting in`inf`

or`nan`

.

## Instances For

`a % b`

computes the remainder upon dividing `a`

by `b`

.
The meaning of this notation is type-dependent.

## Instances For

`a >>> b`

computes `a`

shifted to the right by `b`

places.
The meaning of this notation is type-dependent.

## Instances For

`a ^ b`

computes `a`

to the power of `b`

.
The meaning of this notation is type-dependent.

## Instances For

`a ++ b`

is the result of concatenation of `a`

and `b`

, usually read "append".
The meaning of this notation is type-dependent.

## Instances For

`-a`

computes the negative or opposite of `a`

.
The meaning of this notation is type-dependent.

## Instances For

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.

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

## Instances For

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.

`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`

.

## Instances For

`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`

.

## Instances For

`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

## Instances For

The membership relation `a ∈ s : Prop`

where `a : α`

, `s : γ`

.

## Instances For

`a ∉ b`

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

.

## Instances For

If `a : α`

and `l : List α`

, then `cons a l`

, or `a :: l`

, is the
list whose first element is `a`

and with `l`

as the rest of the list.

## Instances For

`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.

## Instances For

`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.

## Instances For

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`

.

## Instances For

If `mf : F (α → β)`

and `mx : F α`

, then `mf <*> mx : F β`

.
In a monad this is the same as `do let f ← mf; x ← mx; pure (f x)`

:
it evaluates first the function, then the argument, and applies one to the other.

To avoid surprising evaluation semantics, `mx`

is taken "lazily", using a
`Unit → f α`

function.

## Instances For

If `x : F α`

and `y : F β`

, then `x <* y`

evaluates `x`

, then `y`

,
and returns the result of `x`

.

To avoid surprising evaluation semantics, `y`

is taken "lazily", using a
`Unit → f β`

function.

## Instances For

If `x : F α`

and `y : F β`

, then `x *> y`

evaluates `x`

, then `y`

,
and returns the result of `y`

.

To avoid surprising evaluation semantics, `y`

is taken "lazily", using a
`Unit → f β`

function.

## Instances For

If `f : α → β`

and `x : F α`

then `f <$> x : F β`

.

## Instances For

`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.

## Instances For

A case tag argument has the form `tag x₁ ... xₙ`

; it refers to tag `tag`

and renames
the last `n`

hypotheses to `x₁ ... xₙ`

.

## Instances For

"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`

.)

## Instances For

`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.

Because lean uses a strict (call-by-value) evaluation strategy, the signature of this
function is problematic in that it would require `t`

and `e`

to be evaluated before
calling the `ite`

function, which would cause both sides of the `if`

to be evaluated.
Even if the result is discarded, this would be a big performance problem,
and is undesirable for users in any case. To resolve this, `ite`

is marked as
`@[macro_inline]`

, which means that it is unfolded during code generation, and
the definition of the function uses `fun _ => t`

and `fun _ => e`

so this recovers
the expected "lazy" behavior of `if`

: the `t`

and `e`

arguments delay evaluation
until `c`

is known.

## Instances For

`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.

## Instances For

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`

.

## Instances For

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)`

.

## Instances For

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`

.

## Instances For

`Subtype p`

, usually written as `{x : α // p x}`

, is a type which
represents all the elements `x : α`

for which `p x`

is true. It is structurally
a pair-like type, so if you have `x : α`

and `h : p x`

then
`⟨x, h⟩ : {x // p x}`

. An element `s : {x // p x}`

will coerce to `α`

but
you can also make it explicit using `s.1`

or `s.val`

.

## Instances For

`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.

## Instances For

The syntax `[a, b, c]`

is shorthand for `a :: b :: c :: []`

, or
`List.cons a (List.cons b (List.cons c List.nil))`

. It allows conveniently constructing
list literals.

For lists of length at least 64, an alternative desugaring strategy is used
which uses let bindings as intermediates as in
`let left := [d, e, f]; a :: b :: c :: left`

to avoid creating very deep expressions.
Note that this changes the order of evaluation, although it should not be observable
unless you use side effecting operations like `dbg_trace`

.

## Instances For

Auxiliary syntax for implementing `[$elem,*]`

list literal syntax.
The syntax `%[a,b,c|tail]`

constructs a value equivalent to `a::b::c::tail`

.
It uses binary partitioning to construct a tree of intermediate let bindings as in
`let left := [d, e, f]; a :: b :: c :: left`

to avoid creating very deep expressions.

## Instances For

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.

## Instances For

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.

## Instances For

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.