fix test

leanprover · Jul 29, 2024 · 5415c61 · 5415c61
1 parent 9ff329e
commit 5415c61
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean
@@ -8,7 +8,7 @@ error: cannot evaluate expression that depends on the `sorry` axiom.
 Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 -/
 #guard_msgs in
-#eval show Nat from False.rec (by decide)
+#eval show Nat from False.elim (by decide)
 
 /--
 warning: declaration uses 'sorry'