Martin Leduc bc07e36688 Fix terminology in L02rw.lean (#81) ...

According to TPIL we "rewrite the goal using a hypothesis".

2025-09-27 14:40:47 +01:00

..

Addition

Typo: remove extra word to

2025-09-26 22:17:35 -07:00

AdvAddition

alternate proof for add_right_eq_self

2024-06-12 14:40:24 +02:00

AdvMultiplication

Remove extra space, that prevent translation

2025-07-11 14:00:36 +02:00

Algorithm

fix: adjust hint text

2025-09-23 22:44:17 +02:00

Implication

Fix typo in Game

2025-09-27 11:57:21 +08:00

LessOrEqual

Small Typo Fix In L07or_symm.lean

2025-06-15 17:13:25 -04:00

Multiplication

add solutions to induction on other vars. #58

2024-03-24 12:36:58 +01:00

OldAdvMultiplication

fix escaped backspaces

2024-03-11 19:10:20 +01:00

OldAdvProposition

fix escaped backspaces

2024-03-11 19:10:20 +01:00

OldFunction

fix escaped backspaces

2024-03-11 19:10:20 +01:00

OldProposition

Fix typo in Game

2025-09-27 11:57:21 +08:00

Power

Update L08pow_pow.lean

2024-06-12 14:38:20 +02:00

Tutorial

Fix terminology in L02rw.lean (#81)

2025-09-27 14:40:47 +01:00

WIPAlgorithm

LemmaTab -> TheoremTab

2024-01-24 15:42:41 +00:00

WIPFuncProg

LemmaTab -> TheoremTab

2024-01-24 15:42:41 +00:00

Addition.lean

removing some TODOs

2023-10-23 13:08:52 +01:00

AdvAddition.lean

delete ne_succ_self level (too hard, never used)

2023-12-22 15:36:39 +00:00

AdvMultiplication.lean

hopefully finished advanced multiplication world!

2023-12-21 22:09:02 +00:00

Algorithm.lean

fix build

2023-10-27 19:43:12 +01:00

Implication.lean

final tinkering with implication and advanced addition world

2023-10-13 14:07:54 +01:00

LessOrEqual.lean

rename le_of_succ_le_succ to succ_le_succ

2023-12-22 15:54:08 +00:00

Map.txt

Update Map.txt

2023-10-26 17:45:59 +02:00

Multiplication.lean

fix typo in Multiplication

2023-10-24 18:22:03 +01:00

OldAdvMultiplication.lean

move all WIP files to level-rewrite branch

2023-10-14 19:57:20 +01:00

Power.lean

desperate attempt to avoid "no text in level intro world" bug

2023-10-12 19:30:39 +01:00

Tutorial.lean

tinkering

2023-10-22 15:50:20 +01:00

WIPHard.lean

move all WIP files to level-rewrite branch

2023-10-14 19:57:20 +01:00

WIPLessThan.lean

move all WIP files to level-rewrite branch

2023-10-14 19:57:20 +01:00

WIPPrime.lean

move all WIP files to level-rewrite branch

2023-10-14 19:57:20 +01:00

WIPTODOFINDIVANLEVELSEvenOdd.lean

move all WIP files to level-rewrite branch

2023-10-14 19:57:20 +01:00