Use #eval!

leanprover-community · Jul 25, 2024 · 6a10790 · 6a10790
1 parent 5f48a2b
commit 6a10790
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/jacobiSym.lean b/test/jacobiSym.lean
@@ -43,6 +43,6 @@ warning: declaration uses 'sorry'
 info: 1
 -/
 #guard_msgs in
-#eval @legendreSym (2 ^ 11213 - 1) sorry 7
+#eval! @legendreSym (2 ^ 11213 - 1) sorry 7
 
 end Csimp