## Stream: general

### Topic: Typo on natural number game

#### 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?

#### 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

#### Kevin Buzzard (Dec 11 2019 at 01:04):

Thanks! Will try to remember to fix :-)

#### 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