ほとんどの演算子の優先順位は明示的な数値で構成されています。名前付きの優先順位レベルは、最小・最大で閉じられた範囲の外側の端を示し、通常、より複雑な構文拡張で使用されます。
prec ::= num
優先順位は、優先順位の和や差で示されることもあります；これらは通常、指定された優先順位の1つに対して相対的な優先順位を割り当てるために使用されます。
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. 最大の優先順位は関数の位置で発生する項をパースするために使用されます。演算子では基本的にこのレベルを使用すべきではありません。なぜなら、関数の適用が他のどの演算子よりも強く束縛されるだろうというユーザの期待を妨げる可能性があるからです。しかし、他の構成が関数適用とどのように相互作用するかを示すより発展した構文拡張では有用です。
prec ::= ...
| Maximum precedence used in term parsers, in particular for terms in
function position (`ident`, `paren`, ...)
引数優先順位は最大優先順位より1つ小さい値です。このレベルは Lean.Parser.Term.fun : termfun や Lean.Parser.Term.do : termdo などのように、関数の引数として扱われる構文を定義するのに便利です。
prec ::= ...
| Precedence used for application arguments (`do`, `by`, ...).
リードの優先順位は引数の優先順位より低く、 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`, ...). 最小の優先順位はある演算子が他のすべての演算子よりも小さく結合することを保証するために使用できます。
prec ::= ...
| Minimum precedence used in term parsers.