Zulip Chat Archive

Stream: new members

Topic: typo in advanced proposition world


view this post on Zulip Miles (Jan 02 2021 at 20:53):

Hi, not sure if this is the right place, but I there's a typo in level 10 of advanced proposition world in the natural number game. Specifically, there should be a comma after repeat {cc}

view this post on Zulip Alex J. Best (Jan 02 2021 at 21:05):

I agree it should be added to make things clearer, but I want to point out that this is more of a quirk of the tactic goal view than anything else. repeat {cc} does close the goal, and there are no goals left after it, as you can see in the game if you add that line (without the comma) gives you the tick mark at the top for completing the level, and lean stops complaining about unsolved goals in the bottom right, its just that without the comma there is no place where you can put your cursor to see the "no goals" message. It really is still a proof though :smile:

view this post on Zulip Miles (Jan 03 2021 at 01:38):

Good point, thanks for pointing it out :)


Last updated: May 15 2021 at 23:13 UTC