丸括弧と山形括弧

1. () はUnit型の唯一の要素。
2. (3) は 3 のこと。型 Nat
3. (3, 4) はペア型 Nat×Nat
4. (3, 4, 5) は Nat×Nat×Nat
5. (3, 4, 5) = (3, (4, 5)) 右結合的な二項演算子
6. .1 は .fst、.2 は .snd
7. ⟨カンマ区切り項目並び⟩ は構造体リテラルの略記。フィールド名を省略できる。ただし、型情報が必須。
8. 山形括弧は \<, \> で入力できる。
9. (⟨⟩ : Unit) はOK。() は、これに型情報が埋め込まれていると思えばよい。

structure Point2D where
  x : Float
  y : Float

#check Point2D.mk 1.0 2.0 -- Point2D
#check {x:= 1.0, y := 2.0 : Point2D} -- Point2D
#check (⟨1.0, 2.0⟩ : Point2D) -- Point2D
#check (⟨⟩ : Unit) -- Unit