-
Notifications
You must be signed in to change notification settings - Fork 0
/
Game.lean
75 lines (58 loc) · 13 KB
/
Game.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
import Game.Levels.Johdanto
import Game.Levels.Peruslogiikka
import Game.Levels.Implikaatio
import Game.Levels.Disjunktio
import Game.Levels.Konjunktio
import Game.Levels.DisjunktioJaKonjunktio
-- import Game.Levels.Aritmetiikka
-- import Game.Levels.Yhteenlasku
-- import Game.Levels.Kertolasku
import Game.Levels.Negaatio
import Game.Levels.UniversaaliKvanttori
import Game.Levels.EksistenssiKvanttori
import Game.Levels.Ekvivalenssi
import Game.Levels.Funktio
Title "Konsruktiivinen logiikka ja formaali todistaminen"
Introduction
"
Tervetuloa konstruktiivisen logiikan ja formaalin todistamisen kurssille!
Kurssin tehtäväalustana käytämme pelimuotoista oppimisympäristöä, jossa pääset opiskelemaan muun muassa logiikan perusteita, formaalia todistamista sekä Lean -todistusassistentin hyödyntämistä todistusten kirjoittamisessa.
## Ohjeet
Tästä alkaa matkasi logiikan, aritmetiikan ja formaalin todistamisen laajaan universumiin.
Haluan antaa hieman ohjeita matkallesi:
1. Näytön oikeasta reunasta löydät käytössäsi olevat työkalut. Ne on jaettu kolmeen kategoriaan: taktiikat, määritelmät ja lauseet. Saat dokumentaation auki klikkaamalla niistä. Ne joiden vieressä on lukko ovat vielä lukittuja, eli niitä ei saa käyttää todistuksessa.
2. Universumin kartta kertoo missä menet tällä hetkellä. Kartassa voi siirtyä eteenpäin voin sellaisiin maailmoihin ja tasoihin, joiden vaatimukset on ratkaistu.
3. Kannattaa lukea kaikki ohjeet mitä tasoissa annetaan. Jotkut identtiseltä vaikuttavat tasot on tarkoitettu ratkaistavaksi eri työkaluilla, jotta oppisit mahdollisimman paljon Leanin työkaluja.
## Kiireisille seikkailijoille
Jos haluat edetä maailmoita ja kenttiä omassa järjestyksessä, valitse Rules-valikosta *relaxed*:
## Edistyksen tallentuminen
Edistyksesi tallentuu automaattisesti siihen selaimeesi, jolla pelaat peliä. Jos haluat tallentaa edistyksesi tiedostoon, avaa hampurilaismenu sivun oikeasta ylänurkasta, ja paina `Download`. Tiedoston avulla voi palauttaa edistyksen `Upload`-nappulasta.
"
Info "
Olemmen pelialustan kehityksessä hyödyntäneet [Lean Game Serverin](https://adam.math.hhu.de/#/) pelien rakennetta sekä joitakin tehtäviä. Haluaisimme erityisesti kiittää:
* **Alkuperäisen Natural Number Game Lean3-version kehittäjät:** Kevin Buzzard, Mohammad Pedramfar
* **Natural Number Game Lean4-version kehittäjät:** Kevin Buzzard, Jon Eugster
* **Set Theory Game kehittäjä:** Daniel J. Velleman
* **A Lean Intro to Logic kehittäjä:** Mark Fischer
* **Pelimoottori:** Alexander Bentkamp, Jon Eugster, Patrick Massot
"
/-! Information to be displayed on the servers landing page. -/
Languages "Finnish"
CaptionShort "Game Template"
CaptionLong "You should use this game as a template for your own game and add your own levels."
-- Prerequisites "" -- add this if your game depends on other games
-- CoverImage "images/cover.png"
Dependency Johdanto → Peruslogiikka
Dependency Peruslogiikka → Implikaatio
Dependency Peruslogiikka → Negaatio
Dependency Peruslogiikka → Ekvivalenssi
Dependency Ekvivalenssi → Konjunktio
Dependency Ekvivalenssi → Disjunktio
Dependency Disjunktio → DisjunktioJaKonjunktio
Dependency Konjunktio → DisjunktioJaKonjunktio
Dependency Implikaatio → UniversaaliKvanttori
Dependency Implikaatio → EksistenssiKvanttori
Dependency Implikaatio → Funktio
/-! Build the game. Show's warnings if it found a problem with your game. -/
MakeGame