大多数运算符优先级由显式数字组成。 指定的优先级表示范围的外边缘，接近最小值或最大值，通常由更多涉及的语法扩展使用。

prec ::=
    num

优先级也可以表示为优先级的和或差；这些通常用于分配与指定优先级之一相关的优先级。

prec ::= ...
    | Addition of precedences. This is normally used only for offsetting, e.g. `max + 1`. prec + prec

prec ::= ...
    | Subtraction of precedences. This is normally used only for offsetting, e.g. `max - 1`. prec - prec

prec ::= ...
    | Parentheses are used for grouping precedence expressions. (prec)

最大优先级用于解析出现在函数位置的术语。 运算符通常不应使用此级别，因为它可能会干扰用户对函数应用程序比任何其他运算符绑定更紧密的期望，但它在涉及更多的语法扩展中很有用，可以指示其他构造如何与函数应用程序交互。

prec ::= ...
    | Maximum precedence used in term parsers, in particular for terms in
function position (`ident`, `paren`, ...)
max

参数优先级比最大优先级低一。 此级别对于定义应被视为函数参数的语法非常有用，例如 Lean.Parser.Term.fun : termfun 或 Lean.Parser.Term.do : termdo。

prec ::= ...
    | Precedence used for application arguments (`do`, `by`, ...). arg

前导优先级低于参数优先级，并且应用于不应作为函数参数出现的自定义语法，例如 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 ``` The *anaphoric let* `let := v` defines a variable called `this`. let。

prec ::= ...
    | Precedence used for terms not supposed to be used as arguments (`let`, `have`, ...). lead

最小优先级可用于确保某个运算符的绑定不如所有其他运算符紧密。

prec ::= ...
    | Minimum precedence used in term parsers. min