search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

automatically add levels as lemmas #55

Closed joneugster closed 1 year ago

joneugster commented 1 year ago

There should be an option to add a Statement automatically as lemma from there on.

Current behaviour

I'm writing Statement my_lemma … and then NewLemma my_lemma in the next level.

Expected behaviour

Statement my_lemma … could do this automatically. If you don't want it to be added, you can simply avoid giving it a name.

joneugster commented 1 year ago

This has been implemented. Statement my_lemma will unlock my_lemma in the docs in the level following. Moreover, if you import the level with import NNG.Levels.Addition.Level_1 then you will have my_lemma in context.