Pietro Monticone
|
e091faf049
|
Update L10annoying.lean
|
2023-10-26 17:46:59 +02:00 |
|
Pietro Monticone
|
11a6f66466
|
Update L09add_sq.lean
|
2023-10-26 17:46:57 +02:00 |
|
Pietro Monticone
|
2e94593604
|
Update L06pow_add.lean
|
2023-10-26 17:46:53 +02:00 |
|
Pietro Monticone
|
e940b00253
|
Update Level_7.lean
|
2023-10-26 17:46:50 +02:00 |
|
Pietro Monticone
|
22f1e99727
|
Update Level_3.lean
|
2023-10-26 17:46:02 +02:00 |
|
Pietro Monticone
|
dbb8729680
|
Update Map.txt
|
2023-10-26 17:45:59 +02:00 |
|
Pietro Monticone
|
90164f341c
|
Update L03le_succ_self.lean
|
2023-10-26 17:45:56 +02:00 |
|
Pietro Monticone
|
8ba2438677
|
Update inequality_world_tactic_notes.txt
|
2023-10-26 17:45:53 +02:00 |
|
Pietro Monticone
|
05f8a809f1
|
Update L01exact.lean
|
2023-10-26 17:45:50 +02:00 |
|
Pietro Monticone
|
7e7bdc6c06
|
Update Definitions.lean
|
2023-10-26 17:45:48 +02:00 |
|
Jon Eugster
|
99e1017361
|
Merge pull request #33 from jonasspinner/patch-1
Small fix for L03add_left_cancel
|
2023-10-24 21:38:09 +02:00 |
|
Jonas Spinner
|
0f5bc451a9
|
Fix L03add_left_cancel
|
2023-10-24 20:50:07 +02:00 |
|
Kevin Buzzard
|
4d7a1c99c1
|
fix typo in statement of le_total
|
2023-10-24 17:55:54 +01:00 |
|
Kevin Buzzard
|
6f7f99798e
|
update GameServer
|
2023-10-24 17:54:16 +01:00 |
|
Kevin Buzzard
|
1326c865b5
|
tinkering with comments and so on
|
2023-10-23 19:22:18 +01:00 |
|
Kevin Buzzard
|
63ec95bca0
|
Merge branch 'main' into LessOrEqual
|
2023-10-23 17:54:46 +01:00 |
|
Kevin Buzzard
|
1b1fcba058
|
update GameServer
|
2023-10-23 17:52:52 +01:00 |
|
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 |
|
Jon Eugster
|
26512db750
|
Merge pull request #32 from nvchhawch/main
Fix accidental removal of `zero_ne_succ`
|
2023-10-20 11:34:45 +02: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
|
959c3f01c7
|
update lean version
|
2023-10-18 14:00:24 +02:00 |
|
joneugster
|
0c99adb0db
|
bump mathlib
|
2023-10-18 11:37:07 +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 |
|
joneugster
|
4be202af23
|
modify lakefile to hide info messages when building
|
2023-10-17 16:05:46 +02:00 |
|
Madjosz
|
ef2c8616d4
|
Fix L07intro2.lean conclusion
|
2023-10-16 20:17:33 +02:00 |
|
joneugster
|
df1e68cc9d
|
remove unnecessary Dependency commands
|
2023-10-16 17:46:50 +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 |
|
joneugster
|
3333a85d02
|
fix induction
|
2023-10-15 01:16:09 +02:00 |
|
joneugster
|
c0483b727a
|
disable unused variable linteer
|
2023-10-14 23:44:03 +02:00 |
|
Kevin Buzzard
|
63ed90139d
|
these need fixing before we can merge to master
|
2023-10-14 22:35:44 +01:00 |
|
Kevin Buzzard
|
d3ffdb507b
|
cases works!
|
2023-10-14 22:34:33 +01:00 |
|
Kevin Buzzard
|
8b805a800c
|
fix naming
|
2023-10-14 22:34:24 +01:00 |
|
Kevin Buzzard
|
a8ad0f37e7
|
compiling more quietly now
|
2023-10-14 22:08:11 +01:00 |
|
joneugster
|
21a36dc8d5
|
custom cases tactic
|
2023-10-14 21:13:06 +02:00 |
|