16 lines
432 B
Lean4
16 lines
432 B
Lean4
import Game.Levels.Tutorial.01_rfl
|
||
import Game.Levels.Tutorial.02_rw
|
||
import Game.Levels.Tutorial.03_rw_practice
|
||
import Game.Levels.Tutorial.04_zero_succ_one
|
||
|
||
|
||
World "Tutorial"
|
||
Title "Tutorial World"
|
||
|
||
Introduction
|
||
"
|
||
In this world we start introducing the natural numbers `ℕ` and addition. We will also learn some basic tactics, which are the tools we will use to prove theorems in this game.
|
||
|
||
Click on \"Next\" to dive right in!
|
||
"
|