Lean do記法 説明 2

Lean

新しく導入する構文は：

  1. 変更可能代入文
  2. 副作用付きif文〈手続き的if文〉

キーワードと構文：

  1. let mut
  2. := 代入の右辺式は純
  3. if-then-else
  4. if-then
  5. unless-do

翻訳：

  1. mutキーワードは、変数が変更可能であることを宣言する。let mut 変数 ← ... は、変更可能変数を初期化する。初期化で副作用が起きる可能性がある。
  2. 変更可能変数は、ネストしたブロック内で同名の変数が次々と作られる。外側の変数はシャドウイングされる。
  3. elseが省略された場合、void値（Unit型の唯一の値）が値となる。セミコロンまたは改行で続くときはvoid値は捨てられる（次のクライスリ射が暗黙に消費する）。
  4. unlessは単なるシンタックスシュガー。