leanprover-community/NNG4

The commentary uses `repeat` which isn't listed in the tactics

Opened this issue · 2 comments

jariji commented

https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Implication/level/11

The post-solution commentary suggests

intro h
rw [add_succ, add_succ, add_zero] at h
repeat apply succ_inj at h
apply zero_ne_succ at h
exact h

but there is no repeat in the tactic list:

image

joneugster commented

I believe this one is by design of the author (aka Kevin Buzzard), similar to how nth_rewrite also does not appear in the list but only in the documentation of rw.

But thanks for all the comments about typos, etc. I will look through them and merge them on the authors behalf next week!

  • 👍1
joneugster commented

@kbuzzard that's actually a point here. So far we have nth_rewrite/nth_rw and repeat rw as "part" of the rw tactic and doc.

But repeat apply isn't really explained.

Should repeat maybe get it's own doc after all?