Jon Eugster
|
46dbb0e7f6
|
fix escaped backspaces
|
2024-03-11 19:10:20 +01:00 |
|
Jon Eugster
|
381a729f3e
|
bump to v4.6.0
|
2024-02-29 17:19:01 +01:00 |
|
Kevin Buzzard
|
26d8cf5395
|
typo
|
2024-02-27 10:14:09 +00:00 |
|
Kevin Buzzard
|
69cca24efd
|
fix accidentally commented-out NewTactic induction
|
2024-02-27 09:15:19 +00:00 |
|
Jon Eugster
|
6658392838
|
disable succ_inj. #50
|
2024-02-20 15:02:06 +01:00 |
|
Jon Eugster
|
30232f30e2
|
bump to v4.5.0
|
2024-02-20 14:54:21 +01:00 |
|
Jon Eugster
|
b922d89325
|
Merge pull request #49 from pitmonticone/main
Fix typo in Definitions.lean
|
2024-02-02 13:02:44 +01:00 |
|
Jon Eugster
|
d24f07df62
|
Merge pull request #47 from Not-Abram/ReturnToTypewriterModeSuggestion
Return to typewriter mode suggestion
|
2024-02-02 13:02:12 +01:00 |
|
Pietro Monticone
|
c8f7f2caaa
|
Update Definitions.lean
|
2024-01-31 12:26:17 +01:00 |
|
Kevin Buzzard
|
923c4fb175
|
update docstrings in implication world
|
2024-01-24 17:50:18 +00:00 |
|
Kevin Buzzard
|
c5b9473978
|
algorithm world fix docstrings
|
2024-01-24 17:45:59 +00:00 |
|
Kevin Buzzard
|
e2ab764f90
|
missed one in power world
|
2024-01-24 17:45:50 +00:00 |
|
Kevin Buzzard
|
c594db1ac5
|
advanced addition world docstrings
|
2024-01-24 17:40:29 +00:00 |
|
Kevin Buzzard
|
8b10a15011
|
power world docstrings
|
2024-01-24 17:37:50 +00:00 |
|
Steven Clontz
|
b248e1cca0
|
add parentheses, consistent language around "modes"
|
2024-01-24 11:33:31 -06:00 |
|
Kevin Buzzard
|
b04402c91f
|
less or equal world docstrings
|
2024-01-24 17:33:31 +00:00 |
|
Abram
|
2112b6c0ac
|
Return to typewriter mode suggestion
|
2024-01-24 11:28:16 -06:00 |
|
Kevin Buzzard
|
44035c33c1
|
docstring update for advanced mult world
|
2024-01-24 17:27:04 +00:00 |
|
Kevin Buzzard
|
23c9e2c7b9
|
docstring update in multiplication world
|
2024-01-24 17:20:25 +00:00 |
|
Kevin Buzzard
|
270a98ce19
|
fix nth_rewrite warning
|
2024-01-24 16:51:35 +00:00 |
|
Kevin Buzzard
|
e180fc9093
|
actually finish tutorial level
|
2024-01-24 16:45:47 +00:00 |
|
Kevin Buzzard
|
8ef6a85c10
|
finish tutorial
|
2024-01-24 16:41:38 +00:00 |
|
Kevin Buzzard
|
9f00207bb7
|
NewLemma -> NewTheorem (global) and "x" -> /-- x -/ (in tutorial and addition)
|
2024-01-24 16:39:45 +00:00 |
|
Kevin Buzzard
|
c0cfd9f733
|
LemmaDoc -> TheoremDoc
|
2024-01-24 15:45:29 +00:00 |
|
Kevin Buzzard
|
56010d0b43
|
LemmaTab -> TheoremTab
|
2024-01-24 15:42:41 +00:00 |
|
Kevin Buzzard
|
2cbb3474df
|
fix quoting in \ne Adv Mult level 6
|
2024-01-24 14:22:46 +00:00 |
|
Kevin Buzzard
|
4cee0fa343
|
peano theoremtab
|
2024-01-23 21:20:26 +00:00 |
|
Kevin Buzzard
|
37dc3984d8
|
Merge branch 'main' of github.com:leanprover-community/NNG4 into main
|
2024-01-23 20:59:37 +00:00 |
|
Kevin Buzzard
|
93b980fc79
|
import algorithm world in advanced addition world
|
2024-01-23 20:59:34 +00:00 |
|
Kevin Buzzard
|
396a350bda
|
use mathlib Apply ... At
|
2024-01-23 19:24:42 +00:00 |
|
Kevin Buzzard
|
b893d5f1b0
|
remove "if I've written it" comment because I now have
|
2023-12-22 16:36:10 +00:00 |
|
Kevin Buzzard
|
9815f76598
|
hx -> h2 in mul_right_eq_one
|
2023-12-22 16:33:02 +00:00 |
|
Kevin Buzzard
|
ab6b56540d
|
Merge branch 'main' into AdvMultiplication
|
2023-12-22 16:08:12 +00:00 |
|
Kevin Buzzard
|
26a39e3459
|
clarify left and right in three way or
|
2023-12-22 15:55:55 +00:00 |
|
Kevin Buzzard
|
e8ba2a5fee
|
tinkering with text
|
2023-12-22 15:54:43 +00:00 |
|
Kevin Buzzard
|
b8a0fd8c64
|
rename le_of_succ_le_succ to succ_le_succ
|
2023-12-22 15:54:08 +00:00 |
|
Kevin Buzzard
|
4219e68302
|
better LemmaTab for le_succ_self
|
2023-12-22 15:46:10 +00:00 |
|
Kevin Buzzard
|
6f8d7062db
|
delete ne_succ_self level (too hard, never used)
|
2023-12-22 15:36:39 +00:00 |
|
Kevin Buzzard
|
11615ca8fe
|
add sample proofs
|
2023-12-22 15:22:19 +00:00 |
|
Kevin Buzzard
|
58818c9895
|
"Mul" tab -> "*" tab
|
2023-12-22 15:22:09 +00:00 |
|
Kevin Buzzard
|
7b66e800d3
|
add "leave world" explanation
|
2023-12-22 15:00:30 +00:00 |
|
Kevin Buzzard
|
cfe1ae17d5
|
hint for add_succ
|
2023-12-22 14:56:28 +00:00 |
|
Kevin Buzzard
|
9e90d25642
|
0 -> $0$ in tutorial
|
2023-12-22 14:54:25 +00:00 |
|
Kevin Buzzard
|
dc0dd30736
|
tidying up
|
2023-12-22 14:18:03 +00:00 |
|
Kevin Buzzard
|
caf6e47ec8
|
hopefully finished advanced multiplication world!
|
2023-12-21 22:09:02 +00:00 |
|
Kevin Buzzard
|
b81f2ecced
|
Advanced multiplication minor reorganisation
|
2023-12-21 17:12:40 +00:00 |
|
Kevin Buzzard
|
633b39d65a
|
add statememt name and lemmadoc
|
2023-12-21 17:12:18 +00:00 |
|
Kevin Buzzard
|
693051fc84
|
Merge branch 'main' into AdvMultiplication
|
2023-12-20 14:17:43 +00:00 |
|
Kevin Buzzard
|
70104f2018
|
tinkering with docs in advanced + world
|
2023-12-20 14:15:21 +00:00 |
|
Kevin Buzzard
|
16e544acb5
|
add le_one and le_two to <= levels
|
2023-12-20 14:06:14 +00:00 |
|