notation の優先順位上問題なさそうに見えるのに，括弧を付けないとエラーになる現象

section
  -- 排他的論理和の記号を定義
  local notation:60 x:60 " ⊕ " y:61 => xor x y

  -- 等号より優先順位が低いという問題でエラーになる
  -- 上では60で定義しているのに，なぜ？
  #check_failure true ⊕ true = false
  #check (true ⊕ true) = false

  -- 集合の直和の記号と被っていた．
  -- 集合の直和記号は等号より優先度が低いからエラーになっていた
  #check Nat ⊕ Fin 2
end

-- ⊕ という記号をオーバーライドする
macro_rules | `($x ⊕ $y) => `(xor $x $y)

-- もう ⊕ が Sum として解釈されることはなく，エラーにならない
#guard true ⊕ true = false
#guard true ⊕ false = true
#guard false ⊕ true = true
#guard false ⊕ false = false

-- 上書きされたので， Sum の意味で ⊕ を使うことはできなくなった
#check_failure Nat ⊕ Fin 2

lean-ja / lean-by-example

notation の優先順位上問題なさそうに見えるのに，括弧を付けないとエラーになる現象 #302