From 5415c61ae9fe904eba85fb100eeb759d4d9a73c9 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 29 Jul 2024 11:24:39 -0700 Subject: [PATCH] fix test --- tests/lean/run/1697.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean index 23534e45511e..bb8d15715c26 100644 --- 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'