natural number game - add left cancel

Stream: new members

[Aram Bingham]

I was working on level (6) in the advanced addition world and I tried to start a solution with:

repeat {rw add_comm},

After I type the comma, then in the top right window it just shows "Lean is busy.." continually thereafter, even if i delete everything or go to another level. I have tried this in both firefox and chrome, and in either case I have to refresh to be able to interact again.

However the solution which uses rw add_comm for each instance without any repeat tactic seems to have no issues. What is happening when you try to pass the repeat?

[Johan Commelin]

Suppose you have x + y somewhere, then rw add_comm will rewrite it to y + x.
Now you ask it to repeat that action, so it will rewrite it to x + y, and then to y + x, and then to...

[Aram Bingham]

I'm guessing maybe lean is busy replacing the expression t+a by a+t and back again forever until it is told to stop?

[Johan Commelin]

So, yeah, "Lean is busy"

[Johan Commelin]

And probably the Web version is not so good at getting "unbusy" if you delete the bad line of code.

[Aram Bingham]

Got it, thanks Johan.

[Aram Bingham]

I guess I had expected it to just make a "single pass" but I can imagine why this other behavior is useful.

[Kevin Buzzard]

Putting Lean into a loop breaks everything in v1.2 of the natural number game. Sorry. I will push v1.3 today, and putting Lean into a loop will still make it loop, but it will be easier to recover -- you hopefully won't lose all progress.

[Reid Barton]

repeat tac isn't aware of anything that is going on--all it does is keep applying tac until it can't any more.

[Aram Bingham]

No problem/thanks Kevin! Very much enjoying the game.