Natural number game question -

Stream: new members

[Shubhadip Ghosh]

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]

Yes, that's definitely a typo.

[Kevin Buzzard]

Is it still broken in the lean 4 version?

[Shubhadip Ghosh]

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

[Scott Morrison]

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

[Shubhadip Ghosh]

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

[Mauricio Collares]

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]

NNG4 version 3.0.2 is a bit confusing :)

[Jon Eugster]

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