Kevin Buzzard
|
e55da341a6
|
fix: remove dot notation on MyNat.succ (#119)
|
2025-09-28 10:40:24 +02:00 |
|
Kevin Buzzard
|
a022b0673d
|
doc: add historical comments about definition of LE.
|
2025-03-14 17:06:32 +00:00 |
|
Kevin Buzzard
|
d52e8bdc7d
|
remove import Mathlib.Tactic
|
2024-12-19 19:41:23 +00:00 |
|
Jon Eugster
|
1a66069e89
|
do not import all of mathlib
|
2024-03-14 10:38:03 +01:00 |
|
Jon Eugster
|
a71cd97373
|
fix pretty-printing of Power. #46
|
2023-12-15 15:22:45 +01:00 |
|
joneugster
|
ea0b19911f
|
fix power
|
2023-11-28 13:37:29 +01:00 |
|
Kevin Buzzard
|
127ebffb6a
|
Replace recursive definitions of algebraic operations with axioms (#41)
change to axiom approach
|
2023-11-22 09:26:49 +01:00 |
|
Kevin Buzzard
|
bf5e06a2c1
|
fix build
|
2023-10-27 19:43:12 +01:00 |
|
Kevin Buzzard
|
18c4ef9db2
|
add decide level
|
2023-10-27 08:26:25 +01:00 |
|
Kevin Buzzard
|
5c36ad316b
|
Peano axiom levels
|
2023-10-27 00:00:06 +01:00 |
|
Kevin Buzzard
|
a01eb1bd00
|
break off implication world
|
2023-10-11 17:53:51 +01:00 |
|
Kevin Buzzard
|
4e1330bb99
|
more advanced addition world
|
2023-10-02 18:59:47 +01:00 |
|
Kevin Buzzard
|
4dc5f5fb10
|
Begin advanced addition world.
|
2023-10-01 20:43:54 +01:00 |
|
Kevin Buzzard
|
107a02d6e6
|
delete/move dead code
|
2023-09-26 16:23:17 +01:00 |
|
Kevin Buzzard
|
73477d4048
|
sort out succ_eq_add_one import issue for hopefully the last time
|
2023-09-26 14:13:41 +01:00 |
|
Kevin Buzzard
|
f07062e913
|
comment out error
|
2023-09-25 19:51:14 +01:00 |
|
Kevin Buzzard
|
b34717a8a1
|
multiplication world tidy-up
|
2023-09-25 09:20:45 +01:00 |
|
Kevin Buzzard
|
b5c51149b5
|
Initial pass at multiplication world
|
2023-09-23 14:31:44 +01:00 |
|
Jon Eugster
|
0a593a9071
|
Merge branch 'addition-revision' into level-rewrite
|
2023-08-11 17:18:47 +02:00 |
|
Jon Eugster
|
284950984f
|
Merge branch 'main' into level-rewrite
|
2023-08-11 15:37:46 +02:00 |
|
Jon Eugster
|
50682613c6
|
cleanup
|
2023-08-07 13:16:14 +02:00 |
|
Jon Eugster
|
17d52178c6
|
Merge branch 'main' into addition-revision
|
2023-08-07 11:28:46 +02:00 |
|
Jon Eugster
|
0e360a13db
|
Merge pull request #15 from hhu-adam/docstrings
better? docstrings
|
2023-08-06 11:33:35 +02:00 |
|
Kevin Buzzard
|
d8f5785d78
|
compiling and tutorial world approx finished
|
2023-08-05 06:16:37 +01:00 |
|
Kevin Buzzard
|
1da2e8f130
|
compiles!
|
2023-08-04 23:39:53 +01:00 |
|
Jon Eugster
|
836f8f6078
|
import Mathlib.Tactic everywhere
|
2023-08-04 17:14:49 +02:00 |
|
Kevin Buzzard
|
f3792e5405
|
better? docstrings
|
2023-08-04 01:49:06 +01:00 |
|
Jon Eugster
|
2604c89284
|
big refactor
|
2023-05-15 15:12:35 +02:00 |
|