Tutorial.lean

import Game.Levels.Tutorial.L01rfl
import Game.Levels.Tutorial.L02rw
import Game.Levels.Tutorial.L03three_eq_sss0
import Game.Levels.Tutorial.L04add_zero
import Game.Levels.Tutorial.L05add_succ
import Game.Levels.Tutorial.L06twoaddtwo
/-!

# Tutorial world

This file defines Tutorial World. Like all worlds, this world
has a name, a title, an introduction, and most importantly
a finite set of levels (imported above). Each level has a
level number defined within it, and that's what determines
the order of the levels.
-/
World "Tutorial"
Title "Tutorial World"

Introduction
"Welcome to tutorial world! In this world we learn the basics
of proving theorems. The boss level of this world
is the theorem `2 + 2 = 4`.

You prove theorems by solving puzzles using tools called *tactics*.
The puzzle is to prove the theorem by applying tactics
in the right order.

Let's learn some basic tactics. Click on \"Start\" below
to begin your quest.
"