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

..

L01rfl.lean

actually finish tutorial level

2024-01-24 16:45:47 +00:00

L02rw.lean

Fix terminology in L02rw.lean (#81)

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

L03two_eq_ss0.lean

actually finish tutorial level

2024-01-24 16:45:47 +00:00

L04rw_backwards.lean

LemmaTab -> TheoremTab

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

L05add_zero.lean

fix escaped backspaces

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

L06add_zero2.lean

LemmaTab -> TheoremTab

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

L07add_succ.lean

finish tutorial

2024-01-24 16:41:38 +00:00

L08twoaddtwo.lean

add parentheses, consistent language around "modes"

2024-01-24 11:33:31 -06:00

simp_doc_being_moved.txt

tutorial revamped

2023-08-25 03:06:35 +01:00