Kevin Buzzard 18c4ef9db2 add decide level

2023-10-27 08:26:25 +01:00

..

Addition.lean

Merge branch 'addition-revision' into level-rewrite

2023-08-11 17:18:47 +02:00

DecidableEq.lean

add decide level

2023-10-27 08:26:25 +01:00

Definition.lean

Merge pull request #15 from hhu-adam/docstrings

2023-08-06 11:33:35 +02:00

Inequality.lean

big refactor

2023-05-15 15:12:35 +02:00

LE.lean

big refactor

2023-05-15 15:12:35 +02:00

Multiplication.lean

multiplication world tidy-up

2023-09-25 09:20:45 +01:00

PeanoAxioms.lean

Peano axiom levels

2023-10-27 00:00:06 +01:00

Power.lean

compiles!

2023-08-04 23:39:53 +01:00

TutorialLemmas.lean

sort out succ_eq_add_one import issue for hopefully the last time

2023-09-26 14:13:41 +01:00