コード例: 等号の優先順位が50であることを検証する

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

37 stars 6 forks source link

コード例: 等号の優先順位が50であることを検証する #301

Closed Seasawher closed 2 months ago

Seasawher commented 3 months ago

infix:51 " strong " => Nat.add

-- きちんと 1 + (2 strong 3) = 6 と解釈される．
-- これは， 等号の優先順位が 51 未満であることを意味する
#check 1 + 2 strong 3 = 6

-- 優先順位を 50 より小さくすると等号より優先順位が低くなる
-- したがってエラーになる
infix:49 " weak " => Nat.add

#check_failure 1 + 2 weak 3 = 6