Zulip Chat Archive

Stream: new members

Topic: natural number game - add left cancel


view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 05 2020 at 05:31):

So, yeah, "Lean is busy"

view this post on Zulip 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.

view this post on Zulip Aram Bingham (May 05 2020 at 05:32):

Got it, thanks Johan.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Aram Bingham (May 05 2020 at 16:54):

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


Last updated: May 17 2021 at 22:15 UTC