repeat1'

Stream: std4

[Scott Morrison]

I made the PR https://github.com/leanprover/std4/pull/115, requesting a variant of repeat' that fails if it makes no progress.

[Shreyas Srinivas]

Suggestion: A more descriptive name perhaps? For e.g. repeat'_with_fail

[Scott Morrison]

I'm not sure with_fail really explains it. repeat_at_least_once would be good. I was simply copying the naming scheme that I think had existed in mathlib3.

[Mario Carneiro]

I'd rather have short tactic names and long documentation than the reverse