NNG: lean hangs at repeat {apply succ_inj}

Stream: new members

[Matt Yan]

world 8 level 2 can be solved by

apply succ_inj,
apply succ_inj,
assumption,

but when I try

repeat {apply succ_inj},

it shows "Lean is busy...." indefinitely.

[Markus Himmel]

Whenever your goal is an equality of two natural numbers, you can apply succ_inj applies and it will produce another goal that is an equality of two numbers. Since repeat continues until the given tactic fails for the first time, repeat { apply succ_inj } will just keep applying succ_inj until the end of time.

[Markus Himmel]

You could try something like repeat { apply succ_inj, try { assumption } }

[Matt Yan]

Thanks!