#eval
#eval
コマンドは、式の値をその場で評価します。
/-- info: 2 -/
#guard_msgs in #eval 1 + 1
-- 階乗関数
def fac : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * fac n
/-- info: 120 -/
#guard_msgs in #eval fac 5
def main : IO Unit :=
IO.println "Hello, world!"
-- `#eval` により一部の IO アクションを実行することもできる
/-- info: Hello, world! -/
#guard_msgs in #eval main
よくあるエラー
式の評価を行うコマンドであるため、型や関数など、評価のしようがないものを与えるとエラーになります。
-- 型は評価できない
/--
error: expression
ℕ
has type
Type
but instance
Lean.MetaEval Type
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
-/
#guard_msgs in #eval Nat
-- 関数そのものも評価できない
/--
error: expression
fun x => x + 1
has type
ℕ → ℕ
but instance
Lean.MetaEval (ℕ → ℕ)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
-/
#guard_msgs in #eval (fun x => x + 1)
一般に、Repr
や ToString
のインスタンスでないような型の項は #eval
に渡すことができません。
例外処理の慣例
Lean および Mathlib では、「関数ではなく定理に制約を付ける」ことが慣例です。 関数の定義域を制限するアプローチだと、 関数を呼び出すたびに、引数が定義域に含まれているか確認する必要が生じて、 面倒になってしまうためです。
-- たとえば、`1 / 0 = 0` となる。
-- ご存じのようにゼロで割るのは除算として定義できないのだが、
-- 除算の定義域を制限する代わりに、`1 / 0 = 0` という出力を割り当てている。
/-- info: 0 -/
#guard_msgs in #eval 1 / 0
-- もちろん、これは `0` であり `1` ではない。
/-- info: 0 -/
#guard_msgs in #eval (1 / 0) * 0
-- 他にも、自然数の引き算は、マイナスの代わりに `0` を返す。
/-- info: 0 -/
#guard_msgs in #eval 1 - 2
-- `1` ではなくて `2` になる。
/-- info: 2 -/
#guard_msgs in #eval (1 - 2) + 2