#guard_msgs を使用する

lean-ja · Apr 11, 2024 · 96b3e72 · 96b3e72
1 parent b5ddb17
commit 96b3e72
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/Src/Theorem.lean b/Src/Theorem.lean
@@ -17,5 +17,8 @@ theorem frac (n : Nat) : Nat :=
   | 0 => 1
   | n + 1 => (n + 1) * frac n
 
--- コメントを外してみてください
--- #eval frac 5
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'frac', and it does not have executable code
+-/
+#guard_msgs in --#
+#eval frac 5