Zulip Chat Archive

Stream: new members

Topic: natural number game - add left cancel

Aram Bingham (May 05 2020 at 05:23):

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 (May 05 2020 at 05:31):

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 (May 05 2020 at 05:31):

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 (May 05 2020 at 05:31):

So, yeah, "Lean is busy"

Johan Commelin (May 05 2020 at 05:32):

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

Aram Bingham (May 05 2020 at 05:32):

Got it, thanks Johan.

Aram Bingham (May 05 2020 at 05:35):

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

Kevin Buzzard (May 05 2020 at 09:55):

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 (May 05 2020 at 11:24):

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 (May 05 2020 at 16:54):

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

Last updated: Dec 20 2023 at 11:08 UTC