Zulip Chat Archive

Stream: new members

Topic: NNG: lean hangs at repeat {apply succ_inj}


Matt Yan (Feb 07 2022 at 05:09):

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 (Feb 07 2022 at 05:49):

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 (Feb 07 2022 at 05:55):

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

Matt Yan (Feb 07 2022 at 06:37):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC