ImperialCollegeLondon natural_number_game issues

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

Apache License 2.0

292 stars 73 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

improper solution to level 6/9 (uses zero_ne_succ)

#134 rmcmanus342 closed 2 months ago
1
'generalizing' is locked at the level it is being introduced.

#133 zadeoglu opened 9 months ago
0
nicer proof for level13.lean

#132 abourque72 opened 11 months ago
0
Tutorial world, Level 4, one single "refl," causes "Proof complete!"

#131 liusida opened 1 year ago
0
Update level1.lean

#130 abuseofnotation opened 1 year ago
0
unknown identifier 'not_iff_imp_false' error on Level 15 in the Inequality world

#129 roozbeh-yz opened 1 year ago
0
Fix missing word in intro.lean

#128 vezwork opened 1 year ago
0
Change name order

#127 Anoushka1406 closed 1 year ago
1
Advanced Addition World - Level 10 and 11

#126 miguel-negrao opened 1 year ago
2
recursion break

#125 orhid opened 2 years ago
2
Some Complaints

#124 EnderGZM opened 2 years ago
1
A typo in "Advanced Addition World Level 5" (inconsistent variable name)

#123 Kaiwen-S opened 2 years ago
0
fix typo on level 6-7

#122 Stevenjin8 closed 2 years ago
0
Minor typo in World 10 Lvl 1

#121 milescalabresi opened 2 years ago
0
Improve wording in multiplication distributivity lemmas

#120 chezbgone closed 2 years ago
0
Added german translation

#119 Lelidle opened 2 years ago
0
"What next?" page

#118 jcommelin opened 3 years ago
0
Advanced Proposition World LV10 bug

#117 micmelesse closed 7 months ago
0
website down

#116 micmelesse closed 3 years ago
3
Fix typo in world5, level6

#115 gruhn opened 3 years ago
0
A motley collection of Corrections, Complaints and (Curious) Suggestions

#114 ghost opened 3 years ago
0
Added "import tactic.tauto -- useful high-powered tactic"

#113 hmonroe closed 12 months ago
0
reward for finishing

#112 kbuzzard opened 3 years ago
0
inductive le world?

#111 kbuzzard opened 3 years ago
0
nth_rewrite

#110 kbuzzard opened 3 years ago
0
Update level1.lean

#109 vihdzp opened 3 years ago
0
save your game

#108 kbuzzard opened 3 years ago
0
Explain 'B_of_A' naming convention for implications 'A->B'

#107 davidblitz opened 3 years ago
1
typo in multn world 1/9

#106 kbuzzard opened 3 years ago
0
Unable to use and_symm theorem in World 7, Level 3

#105 Gunjeet-Singh opened 4 years ago
0
Bug in first two levels of the Power World

#104 czAdamV closed 4 years ago
1
How to apply Leibniz's law for equality?

#103 darijgr opened 4 years ago
3
Undocumented implicit variables in Advanced Addition World

#102 darijgr opened 4 years ago
0
Add ability to toggle between rendered view and literal lean

#101 al-yisun opened 4 years ago
0
Shorten the proof of not_succ_le_self.

#100 Julian closed 4 years ago
1
Some solutions use `assumption` which isn't mentioned in the text

#99 Julian opened 4 years ago
0
Mark things as irreducible?

#98 shingtaklam1324 opened 4 years ago
0
fold away hints

#97 kbuzzard opened 4 years ago
0
Typo in world 3 level 1

#96 baldoalessandro opened 4 years ago
0
Tutorial world fully translated to French

#95 ADedecker opened 4 years ago
0
world 7 level 8 "did you spot the import?"

#94 kbuzzard opened 4 years ago
0
Reuse the proof from the solution to level 16

#93 eric-wieser opened 4 years ago
0
World 10, level 16: Simplify the proof even further, using an earlier result

#92 eric-wieser opened 4 years ago
0
Sian Carey fellowship

#91 kbuzzard opened 4 years ago
0
More French translation

#90 sgouezel closed 4 years ago
0
explain implicit inputs

#89 kbuzzard opened 4 years ago
0
Advanced Proposition world: Level 1/10

#88 arademaker closed 4 years ago
1
Drop down menu for levels

#87 pglutz closed 4 years ago
2
Update level1.lean

#86 arademaker closed 4 years ago
0
Update level1.lean

#85 arademaker closed 4 years ago
1