greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix nth_rewrite warning

Browse Source
This commit is contained in:
Kevin Buzzard
2024-01-24 16:51:35 +00:00
parent e180fc9093
commit 270a98ce19
2 changed files with 14 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
Game/Levels/Tutorial/L02rw.lean
View File

@@ -138,6 +138,20 @@ will change the goal to `succ 1 + succ 1 = 4`.
-/
TacticDoc «repeat»
/--
## Summary
If `h : X = Y` and there are several `X`s in the goal, then
`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.
## Example
If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`
will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
will change the goal to `succ 1 + succ 1 = 4`.
-/
TacticDoc nth_rewrite
NewTactic rw
NewHiddenTactic «repeat» nth_rewrite

16
Game/Levels/Tutorial/L08twoaddtwo.lean
View File

@@ -10,22 +10,6 @@ TheoremTab "012"
namespace MyNat
/--
## Summary
If `h : X = Y` and there are several `X`s in the goal, then
`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.
## Example
If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`
will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
will change the goal to `succ 1 + succ 1 = 4`.
-/
TacticDoc nth_rewrite
NewHiddenTactic nth_rewrite
Introduction
" Good luck!