() はUnit型の唯一の要素。 (3) は 3 のこと。型 Nat (3, 4) はペア型 Nat×Nat (3, 4, 5) は Nat×Nat×Nat (3, 4, 5) = (3, (4, 5)) 右結合的な二項演算子 .1 は .fst、.2 は .snd ⟨カンマ区切り項目並び⟩ は構造体リテラルの略記。フィールド名を省略できる…

関数適用は必ず空白が必要。空白類が適用演算子の記号だから。一方、x.2 や x[3] のようなタプル／リスト／配列へのアクセスは、空白を入れてはダメ。空白が適用演算子なので、適用として解釈されてエラーになる。だいぶハマる。

シンボル上にマウスホバーでツールチップが出る。 シンボル上でホバーから[ctrl+click]で定義元にジャンプ。 必要なら[shift+ctrl+enter]でインフォビューをON/OFF とりあえず[F12]だが、トンチンカンな所に飛ぶことがある。 [alt+←]で戻る。 [alt+F12]でpee…