Most operator precedences consist of explicit numbers. The named precedence levels denote the outer edges of the range, close to the minimum or maximum, and are typically used by more involved syntax extensions.
prec ::= num
Precedences may also be denoted as sums or differences of precedences; these are typically used to assign precedences that are relative to one of the named precedences.
prec ::= ...
| Addition of precedences. This is normally used only for offsetting, e.g. `max + 1`. prec ::= ...
| Subtraction of precedences. This is normally used only for offsetting, e.g. `max - 1`. prec ::= ...
| Parentheses are used for grouping precedence expressions. The maximum precedence is used to parse terms that occur in a function position. Operators should typically not use use this level, because it can interfere with users' expectation that function application binds more tightly than any other operator, but it is useful in more involved syntax extensions to indicate how other constructs interact with function application.
prec ::= ...
| Maximum precedence used in term parsers, in particular for terms in
function position (`ident`, `paren`, ...)
Argument precedence is one less than the maximum precedence.
This level is useful for defining syntax that should be treated as an argument to a function, such as Lean.Parser.Term.fun : termfun or Lean.Parser.Term.do : termdo.
prec ::= ...
| Precedence used for application arguments (`do`, `by`, ...).
Lead precedence is less that argument precedence, and should be used for custom syntax that should not occur as a function argument, such as Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
let.
prec ::= ...
| Precedence used for terms not supposed to be used as arguments (`let`, `have`, ...). The minimum precedence can be used to ensure that an operator binds less tightly than all other operators.
prec ::= ...
| Minimum precedence used in term parsers.