Zulip Chat Archive

Stream: new members

Topic: Natural number game question -

Shubhadip Ghosh (Jul 23 2023 at 06:32):

Hi, I have a doubt. In level 3 (Peano axiom) of the Natural Number Game, the exercise is 'If succ(a)=b, then succ(succ(a))=succ(a)'. Is the right-hand side of the conclusion part will be 'succ(b)' instead of 'succ(a)'

Yaël Dillies (Jul 23 2023 at 06:45):

Yes, that's definitely a typo.

Kevin Buzzard (Jul 23 2023 at 06:48):

Is it still broken in the lean 4 version?

Shubhadip Ghosh (Jul 23 2023 at 07:34):

I am doing it from the direct link given in the resource section where version number is 3.0.2.

Scott Morrison (Jul 23 2023 at 23:38):

@Shubhadip Ghosh, could you show us where this link appears, so we can remove it?

Shubhadip Ghosh (Jul 24 2023 at 00:04):

Here is the link: https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/Tutorial/level/3

Mauricio Collares (Jul 24 2023 at 07:46):

Oh, you mean 3.0.2 is the Natural Number Game version (as in https://github.com/hhu-adam/NNG4/blob/4687e0bd7c30581423957a1d4e176024d374cd1d/Game.lean#L19)

Mauricio Collares (Jul 24 2023 at 07:47):

NNG4 version 3.0.2 is a bit confusing :)

Jon Eugster (Jul 24 2023 at 20:49):

Maybe we should bump that version number to 4.x.x skipping 3.x entirely (Kevins lean3 version was 2.x) :grinning_face_with_smiling_eyes:

Thanks, Ill try to fix that typo tomorrow

Last updated: Dec 20 2023 at 11:08 UTC