`notation`¶

Lean では，標準的な定義だけでなく，数学に近い記号や専用の構文を定義できます．たとえば α → β は関数型の notation，P ∧ Q は And P Q の notation，x ∈ s は membership の notation です．このような notation は，elaboration の過程で既存の定義や関数を使う式へ結びつけられます．

小さな notation なら，notation や infix で定義できます．

notation "twice(" n ")" => n + n

example : twice(3) = 6 := by
  rfl

infixl:65 " +++ " => Nat.add

example : 2 +++ 3 = 5 := by
  rfl

notation "twice(" n ")" => n + n は，twice(3) という notation を 3 + 3 と読むようにする指定です． infixl:65 " +++ " => Nat.add は，中置 notation x +++ y を Nat.add x y と読むようにする指定です． 65 は優先順位，infixl の l は左結合を表します．

実際の Mathlib では，ℝ，∑，∈，⊔，→+* など，多くの notation が定義されています． notation は読みやすさのための糖衣構文なので，分からない notation に出会ったら，まず #check で型を確認し，「これはどの定義の別表記か」を調べるのが有効です．講義資料では notation を使いますが，必要に応じて元の定義名も併記します．

notation¶

`notation`¶