Zulip Chat Archive

Stream: general

Topic: Typo on natural number game


view this post on Zulip YH (Dec 10 2019 at 19:23):

In Inequality world, Level 3

Our hypothesis h is now ∃ (c : mynat), b = a + c (or a ≤ b if you elected not to do the definitional rewriting) so

cases h with c hc,

gives you the natural number c and the hypothesis hc : b = a + d.

Shouldn't the last one be hc : b = a + c?

view this post on Zulip David Renshaw (Dec 10 2019 at 20:04):

I agree! You could submit a pull request correcting it: https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world10/level3.lean#L34

view this post on Zulip Kevin Buzzard (Dec 11 2019 at 01:04):

Thanks! Will try to remember to fix :-)

view this post on Zulip YH (Dec 11 2019 at 01:11):

I agree! You could submit a pull request correcting it: https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world10/level3.lean#L34

Great. I just did.

Also https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world8/level1.lean#L20
this one should be succ_inj {a b : mynat} : (since it is used as succ_inj(hs) without specifying a and b) but I'm not sure if just changing it here will be enough to change it everywhere in the game so I didn't propose a change.


Last updated: May 12 2021 at 23:13 UTC