299 Commits

Author SHA1 Message Date
Kevin Buzzard
89b751356e more tutorial tinkering 2023-08-25 02:56:40 +01:00
Kevin Buzzard
5de7fadb89 tutorial world rethink 2023-08-25 02:22:38 +01:00
Kevin Buzzard
6295a75475 fix build! 2023-08-24 22:55:08 +01:00
Kevin Buzzard
bf95188254 note to make add_Zero a function 2023-08-24 22:43:27 +01:00
Jon Eugster
b41a35d56c bump gameserver after fixes 2023-08-12 12:35:29 +02:00
Kevin Buzzard
8ecb0be912 add placeholder level to each world 2023-08-12 05:27:45 +01:00
Kevin Buzzard
cbaeb0452c making the full graph 2023-08-12 05:01:29 +01:00
Jon Eugster
720f3320eb some fixes 2023-08-11 17:57:14 +02:00
Jon Eugster
0a593a9071 Merge branch 'addition-revision' into level-rewrite 2023-08-11 17:18:47 +02:00
Jon Eugster
79ebd39feb small fixes 2023-08-11 17:12:34 +02:00
Jon Eugster
284950984f Merge branch 'main' into level-rewrite 2023-08-11 15:37:46 +02:00
Jon Eugster
868d8d9d71 bump gameserver 2023-08-11 15:06:01 +02:00
Kevin Buzzard
7fb639142d fixes 2023-08-10 19:37:16 +01:00
Kevin Buzzard
1fa4150410 add TODO 2023-08-07 12:16:54 +01:00
Jon Eugster
50682613c6 cleanup 2023-08-07 13:16:14 +02:00
Kevin Buzzard
b517673ea2 fix maths mode 2023-08-07 12:10:50 +01:00
Kevin Buzzard
5049f0a6a1 numeral fixes 2023-08-07 11:57:45 +01:00
Kevin Buzzard
496c1ccb41 fix typo 2023-08-07 11:22:49 +01:00
Kevin Buzzard
a16c0fa51d ac_rfl idea 2023-08-07 10:52:11 +01:00
Jon Eugster
749e24d6c0 bump gameserver, introduce doc comments for statement description 2023-08-07 11:49:31 +02:00
Jon Eugster
17d52178c6 Merge branch 'main' into addition-revision 2023-08-07 11:28:46 +02:00
Kevin Buzzard
060e4f4576 final levels of addition world 2023-08-07 09:38:13 +01:00
Jon Eugster
c80a695def enable ac_rfl 2023-08-06 23:28:11 +02:00
Kevin Buzzard
9de6f45fa6 tidying up now I can see my work in a browser 2023-08-05 18:33:53 +01:00
Kevin Buzzard
5e4ee9be02 addition world is 1/3 go 2023-08-05 07:35:21 +01:00
Kevin Buzzard
f82848a012 addition to first sub-boss 2+2=4 2023-08-05 07:29:05 +01:00
Kevin Buzzard
84a7465636 Merge branch 'tutorial-revision' into addition-revision 2023-08-05 06:20:07 +01:00
Kevin Buzzard
d8f5785d78 compiling and tutorial world approx finished 2023-08-05 06:16:37 +01:00
Kevin Buzzard
aff078d995 level 4 namechange 2023-08-05 04:27:49 +01:00
Kevin Buzzard
b2ec28cbff Merge branch 'main' into addition-revision 2023-08-05 04:11:54 +01:00
Kevin Buzzard
1da2e8f130 compiles! 2023-08-04 23:39:53 +01:00
Kevin Buzzard
a1160d782b add succ_ne_zero etc to a basic logic file not for t
eaching
2023-08-04 23:23:21 +01:00
Kevin Buzzard
a14e4af3f7 fix imports 2023-08-04 22:51:26 +01:00
Kevin Buzzard
f7cc4b13c9 change Game file so only one world! 2023-08-04 22:51:11 +01:00
Kevin Buzzard
c8f0f8fa55 Merge branch 'main' into tutorial-revision 2023-08-04 21:34:38 +01:00
Kevin Buzzard
22869e7ae3 add subbosses 2023-08-04 21:31:39 +01:00
Kevin Buzzard
9c211e94da tutorial world revamp 2023-08-04 21:30:07 +01:00
Jon Eugster
e6d786fc2c remove debugging code 2023-08-04 17:15:33 +02:00
Jon Eugster
836f8f6078 import Mathlib.Tactic everywhere 2023-08-04 17:14:49 +02:00
Kevin Buzzard
04ae200ec6 Merge branch 'main' into tutorial-revision 2023-08-04 12:50:28 +01:00
Kevin Buzzard
d1c06d8e6b addition notes 2023-08-04 04:51:31 +01:00
Kevin Buzzard
484813fbe9 more tutorial edits 2023-08-04 01:38:30 +01:00
Kevin Buzzard
5faad0d5ba initial modification of tutorial level 2023-08-03 20:37:06 +01:00
Jon Eugster
47b278783e fixes 2023-07-20 16:11:24 +02:00
Jon Eugster
ba13a9633c bump Gameserver 2023-07-19 14:58:22 +02:00
Balazs Endresz
e0f63f96a4 typo 2023-05-20 20:05:04 +02:00
Balazs Endresz
378a156bbe typos 2023-05-16 23:41:53 +02:00
Jon Eugster
b04341c0c4 optional statement 2023-05-15 18:00:00 +02:00
Jon Eugster
2604c89284 big refactor 2023-05-15 15:12:35 +02:00