Kevin Buzzard
|
8f997c267e
|
Merge branch 'main' into LessOrEqual
|
2023-10-23 13:52:23 +01:00 |
|
Kevin Buzzard
|
417dba426c
|
Add new left/right tactic practice world plus tactic docs
|
2023-10-23 13:44:16 +01:00 |
|
Kevin Buzzard
|
cedc46846d
|
add mystical ancient tactic
|
2023-10-23 13:43:48 +01:00 |
|
Kevin Buzzard
|
2d16f7f3b3
|
removing some TODOs
|
2023-10-23 13:08:52 +01:00 |
|
Kevin Buzzard
|
674008ecc1
|
superficial edit so I can recompile and look at warnings
|
2023-10-22 16:25:59 +01:00 |
|
Kevin Buzzard
|
b8e530f6e0
|
reinstate IGiveUp
|
2023-10-22 16:13:36 +01:00 |
|
Kevin Buzzard
|
7944403651
|
struggling with add_succ + succ_eq_add_one
|
2023-10-22 16:13:28 +01:00 |
|
Kevin Buzzard
|
43768d0dfe
|
tinkering with rw backwards level
|
2023-10-22 16:04:33 +01:00 |
|
Kevin Buzzard
|
b860446836
|
Merge branch 'main' into LessOrEqual
|
2023-10-22 15:54:38 +01:00 |
|
Kevin Buzzard
|
d80a520359
|
tinkering
|
2023-10-22 15:50:20 +01:00 |
|
Kevin Buzzard
|
c1addcbe86
|
adv multn world sketch
|
2023-10-21 19:00:35 +01:00 |
|
Kevin Buzzard
|
f71a55045a
|
update to lean and fixes
|
2023-10-21 19:00:23 +01:00 |
|
Naman Chhawchharia
|
b18d5667c2
|
Add zero_ne_succ
|
2023-10-19 11:56:38 -04:00 |
|
joneugster
|
2d26496e96
|
cleanup NewTactic entries
|
2023-10-19 12:06:49 +02:00 |
|
joneugster
|
be8afc3797
|
fix nth_rewrite not unlocking
|
2023-10-19 11:05:23 +02:00 |
|
joneugster
|
5ca0aec981
|
typo #30
|
2023-10-17 16:14:11 +02:00 |
|
Jon Eugster
|
4631fa2cfd
|
Merge pull request #29 from Madjosz/patch-1
Fix L07intro2.lean conclusion
|
2023-10-17 16:12:13 +02:00 |
|
joneugster
|
75bb4e5f86
|
remove unecessary NewLemma
|
2023-10-17 16:09:27 +02:00 |
|
Madjosz
|
ef2c8616d4
|
Fix L07intro2.lean conclusion
|
2023-10-16 20:17:33 +02:00 |
|
joneugster
|
2fc242d3f5
|
improve hint in implication lvl 4 #28
|
2023-10-16 16:32:24 +02:00 |
|
joneugster
|
1dbfaae51c
|
the tactic of tactics
|
2023-10-15 03:17:30 +02:00 |
|
Kevin Buzzard
|
d3ffdb507b
|
cases works!
|
2023-10-14 22:34:33 +01:00 |
|
Kevin Buzzard
|
a8ad0f37e7
|
compiling more quietly now
|
2023-10-14 22:08:11 +01:00 |
|
Kevin Buzzard
|
aa6bb6db91
|
pedagogical change in apply intro level
|
2023-10-14 20:04:16 +01:00 |
|
Kevin Buzzard
|
20bc9fe61d
|
move all WIP files to level-rewrite branch
|
2023-10-14 19:57:20 +01:00 |
|
Kevin Buzzard
|
48b0ea2bc6
|
big tidy-up
|
2023-10-14 19:47:21 +01:00 |
|
Kevin Buzzard
|
b260a53f82
|
get game building again!
|
2023-10-14 19:09:15 +01:00 |
|
Kevin Buzzard
|
2cd3b9a47b
|
adding more lemmadocs
|
2023-10-14 18:45:55 +01:00 |
|
Kevin Buzzard
|
124aaaef7e
|
Merge branch 'level-rewrite' of github.com:hhu-adam/NNG4 into level-rewrite
|
2023-10-14 17:14:30 +01:00 |
|
Kevin Buzzard
|
6ec6907707
|
edits in LE world
|
2023-10-14 17:11:22 +01:00 |
|
Kevin Buzzard
|
378acfd9ec
|
initial version of seven <= levels
|
2023-10-13 23:50:28 +01:00 |
|
Kevin Buzzard
|
d91efb2443
|
tinkering
|
2023-10-13 19:51:12 +01:00 |
|
Kevin Buzzard
|
7e4226ec25
|
start on <= world
|
2023-10-13 19:11:24 +01:00 |
|
Kevin Buzzard
|
39a9c26a98
|
final tinkering with implication and advanced addition world
|
2023-10-13 14:07:54 +01:00 |
|
Kevin Buzzard
|
cb7a727099
|
finish plan for NNG4
|
2023-10-12 21:30:12 +01:00 |
|
Kevin Buzzard
|
93ef8aae4c
|
fix typo in zero_mul (thanks Jo)
|
2023-10-12 21:12:53 +01:00 |
|
Kevin Buzzard
|
78a0b03acf
|
desperate attempt to avoid "no text in level intro world" bug
|
2023-10-12 19:30:39 +01:00 |
|
Kevin Buzzard
|
8e56a06ef2
|
fix quoted backslash
|
2023-10-12 18:32:55 +01:00 |
|
Kevin Buzzard
|
bf013af673
|
Merge branch 'main' into level-rewrite
|
2023-10-11 17:58:40 +01:00 |
|
Kevin Buzzard
|
a01eb1bd00
|
break off implication world
|
2023-10-11 17:53:51 +01:00 |
|
Jon Eugster
|
dc7c7d451b
|
Merge pull request #20 from wupr/main
Remove reference to Prop in the Function World
|
2023-10-10 10:04:30 +02:00 |
|
Kevin Buzzard
|
2b431544d8
|
inequality world notes
|
2023-10-09 07:55:22 +01:00 |
|
Kevin Buzzard
|
3da1dda4eb
|
add new tutorial level
|
2023-10-09 07:54:47 +01:00 |
|
Kevin Buzzard
|
5f3f51144a
|
a little tidying
|
2023-10-05 14:16:57 +01:00 |
|
Kevin Buzzard
|
8a03ea3388
|
advanced addition world almost done
|
2023-10-05 14:15:46 +01:00 |
|
Kevin Buzzard
|
4325af4757
|
start on key advanced addition world
|
2023-10-05 11:16:50 +01:00 |
|
Kevin Buzzard
|
23593c1279
|
editing tutorial world
|
2023-10-04 23:23:36 +01:00 |
|
Kevin Buzzard
|
6c8264ec37
|
fix level number
|
2023-10-04 23:23:26 +01:00 |
|
Kevin Buzzard
|
a53f74a627
|
fix typos spotted by Damiano
|
2023-10-04 16:32:05 +01:00 |
|
Kevin Buzzard
|
0e36f7d8f7
|
apply at!
|
2023-10-04 15:43:57 +01:00 |
|