minor update

lean-dojo · Sep 17, 2023 · 6b4211f · 6b4211f
1 parent e4377a3
commit 6b4211f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Examples.lean b/Examples.lean
@@ -1,7 +1,7 @@
 import LeanInfer
 
 example (a b c : Nat) : a + b + c = a + c + b := by
-  suggest_tactics!
+  suggest_tactics
   sorry
 
 example (a b c : Nat) : a + b + c = a + c + b := by