Zulip Chat Archive

Stream: general

Topic: natural number game


Oliver Fuchs (Jun 16 2021 at 05:18):

3:49 PM

Hi, I am new in natural number game. I have to proof succ(a)b=ab+b but i cant. But i can proof add_mul by my own. With this I can proof succ(a)b=ab+b. How can I add add_mul as theorem to the multiplication world? thans.

Mario Carneiro (Jun 16 2021 at 05:38):

You should be able to use all proofs you have done in previous levels

Mario Carneiro (Jun 16 2021 at 05:39):

so once you have done add_mul you can use apply add_mul or rw add_mul or have := add_mul a b c to use the add_mul theorem

Oliver Fuchs (Jun 16 2021 at 05:48):

Thanks, I tried already to install Lean on my computer. There it must be possible to start my own natural number game.
But the import advises

import mynat.definition -- imports the natural numbers {0,1,2,3,4,...}.
import mynat.add -- imports definition of addition on the natural numbers.
import mynat.mul -- imports definition of multiplication on the natural numbers.
gave an error. How can I import these definitioins?

Mario Carneiro (Jun 16 2021 at 05:55):

I don't think NNG is intended for offline use, but I think it's possible if you download the NNG repo

Kevin Buzzard (Jun 16 2021 at 05:55):

You should install leanproject following the instructions on the community website and then use it to install the natural number game

Gihan Marasingha (Jul 02 2021 at 10:54):

I'm using the NNG platform to write some games but I find, for some reason, that adding locale/content.pot to .gitignore has no effect. Has anyone else had this issue?

Never mind. I figured out that I needed to do git rm --cached locale/content.pot first.

Kevin Buzzard (Jul 02 2021 at 11:49):

I'd love to set what you come up with! Things like the complex number game could probably be made into web apps via this. There's also a good filter game one could make

Gihan Marasingha (Jul 02 2021 at 12:33):

Oooh, I had been thinking about a filter game (I was inspired by your TCC course) and that's next on my list. At the moment, I'm doing an even more basic intro to Lean that the NNG, focussing on using rewrites to manipulate integer equations.

Kevin Buzzard (Jul 02 2021 at 19:59):

Interesting!

Kevin Buzzard (Jul 02 2021 at 20:00):

Let me know if you want beta testers (give James a URL and he can advertise it on the Discord)

Gihan Marasingha (Jul 02 2021 at 21:01):

Thanks. Will do!


Last updated: Dec 20 2023 at 11:08 UTC