clarify simp_add

2023-11-16 15:20:04 -06:00
parent 7ed6c4b4a6
commit 1b76917f1b
1 changed files with 2 additions and 2 deletions
--- 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!
 "