src/Init/Notation.lean からの情報。
構文範疇precは項の優先度を表す値（の表現）のことで：
- 項の優先度： max = 1024, arg = 1023, lead = 1022, min = 10
- パイプ記号 <|, |> は優先度は min = 10
- =, ∈ が50
- 足し算は65、
- 規表現風接尾辞の *,+,? は arg = 1023
Swiftの演算子がよく整理されている。Leanの値は後で埋める。
| 演算子 | 説明 | 結合律 | 優先順位 | Lean |
| << | 左ビットシフト | 無結合 | 160 | |
| >> | 右ビットシフト | 無結合 | 160 | |
| * | 乗算 | 左結合 | 160 | |
| / | 除算 | 左結合 | 160 | |
| % | 剰余 | 左結合 | 160 | |
| & | ビットAND | 左結合 | 160 | |
| + | 加算 | 左結合 | 140 | 65 |
| - | 減算 | 左結合 | 140 | |
| 縦棒 | ビットOR | 左結合 | 140 | |
| ^ | ビットXOR | 左結合 | 140 | |
| < | 未満 | 無結合 | 130 | |
| <= | 以下 | 無結合 | 130 | |
| > | より上 | 無結合 | 130 | |
| >= | 以上 | 無結合 | 130 | |
| == | イコール | 無結合 | 130 | 50 |
| != | ノットイコール | 無結合 | 130 | |
| ~= | パターンマッチ | 無結合 | 130 | |
| && | 論理AND | 左結合 | 120 | |
| 二本縦棒 | 論理OR | 左結合 | 110 | |
| ?: | 三項条件 | 右結合 | 100 | |
| = | 代入 | 右結合 | 90 | |
| = | 乗算と代入 | 右結合 | 90 | |
|---|---|---|---|---|
| += | 加算と代入 | 右結合 | 90 | |
| &:&= | 論理ANDと代入 | 右結合 | 90 |
優先度のグループ分けは：
- BitwiseShiftPrecedence << など 160
- MultiplicationPrecedence * など 160
- AdditionPrecedence + など 140
- RangeFormationPrecedence ... など 135
- CastingPrecedence is など 132
- NilCoalescingPrecedence ?? など 131
- ComparisonPrecedence = など 130
- LogicalConjunctionPrecedence && など 130
- LogicalDisjunctionPrecedence || など 120
- TernaryPrecedence ?: など 100
- AssignmentPrecedence = など 90
130代が混みすぎ。
