greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

make compiling faster

Browse Source
This commit is contained in:
Kevin Buzzard
2023-08-05 04:03:55 +01:00
parent 22869e7ae3
commit 7faf4321ba
1 changed files with 7 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
Game.lean
View File

@@ -2,13 +2,13 @@ import GameServer.Commands
import Game.Levels.Tutorial
import Game.Levels.Addition
import Game.Levels.Multiplication
import Game.Levels.Power
import Game.Levels.Function
import Game.Levels.Proposition
import Game.Levels.AdvProposition
import Game.Levels.AdvAddition
import Game.Levels.AdvMultiplication
--import Game.Levels.Multiplication
--import Game.Levels.Power
--import Game.Levels.Function
--import Game.Levels.Proposition
--import Game.Levels.AdvProposition
--import Game.Levels.AdvAddition
--import Game.Levels.AdvMultiplication
--import Game.Levels.Inequality
Title "Natural Number Game"