Merge pull request #43 from StevenClontz/patch-1

clarify simp_add
leanprover-community · Nov 17, 2023 · 0e18fd8 · 0e18fd8
2 parents 7ed6c4b + 1b76917
commit 0e18fd8
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Game/Levels/Algorithm/L04add_algo3.lean b/Game/Levels/Algorithm/L04add_algo3.lean
@@ -28,9 +28,9 @@ This code here
 macro \"simp_add\" : tactic => `(tactic|(
   simp only [add_assoc, add_left_comm, add_comm]))
 ```
-creates a new tactic `simp_add`, which runs
+was used to create a new tactic `simp_add`, which runs
 `simp only [add_assoc, add_left_comm, add_comm]`.
-Try it!
+Try running `simp_add` to solve this level!
 "