ImperialCollegeLondon/natural_number_game

Issues

• improper solution to level 6/9 (uses zero_ne_succ)

  #134 opened 4 months ago by rmcmanus342
  1

• Advanced Proposition World LV10 bug

  #117 opened 9 months ago by micmelesse
  0

• 'generalizing' is locked at the level it is being introduced.

  #133 opened 10 months ago by zadeoglu
  0

• Tutorial world, Level 4, one single "refl," causes "Proof complete!"

  #131 opened a year ago by liusida
  0

• unknown identifier 'not_iff_imp_false' error on Level 15 in the Inequality world

  #129 opened a year ago by roozbeh-yz
  0

• Advanced Addition World - Level 10 and 11

  #126 opened 2 years ago by miguel-negrao
  2

• recursion break

  #125 opened 2 years ago by orhid
  2

• Some Complaints

  #124 opened 2 years ago by EnderGZM
  1

• A typo in "Advanced Addition World Level 5" (inconsistent variable name)

  #123 opened 3 years ago by Kaiwen-S
  0

• Minor typo in World 10 Lvl 1

  #121 opened 3 years ago by milescalabresi
  0

• "What next?" page

  #118 opened 3 years ago by jcommelin
  0

• website down

  #116 opened 3 years ago by micmelesse
  3

• A motley collection of Corrections, Complaints and (Curious) Suggestions

  #114 opened 3 years ago
  0

• reward for finishing

  #112 opened 4 years ago by kbuzzard
  0

• How to apply Leibniz's law for equality?

  #103 opened 4 years ago by darijgr
  3

• inductive le world?

  #111 opened 4 years ago by kbuzzard
  0

• nth_rewrite

  #110 opened 4 years ago by kbuzzard
  0

• save your game

  #108 opened 4 years ago by kbuzzard
  0

• Explain 'B_of_A' naming convention for implications 'A->B'

  #107 opened 4 years ago by davidblitz
  1

• typo in multn world 1/9

  #106 opened 4 years ago by kbuzzard
  0

• Unable to use and_symm theorem in World 7, Level 3

  #105 opened 4 years ago by Gunjeet-Singh
  0

• Bug in first two levels of the Power World

  #104 opened 4 years ago by czAdamV
  1

• Undocumented implicit variables in Advanced Addition World

  #102 opened 4 years ago by darijgr
  0

• Add ability to toggle between rendered view and literal lean

  #101 opened 4 years ago by al-yisun
  0

• Some solutions use `assumption` which isn't mentioned in the text

  #99 opened 4 years ago by Julian
  0

• Mark things as irreducible?

  #98 opened 4 years ago by shingtaklam1324
  0

• fold away hints

  #97 opened 4 years ago by kbuzzard
  0

• Typo in world 3 level 1

  #96 opened 4 years ago by baldoalessandro
  0

• world 7 level 8 "did you spot the import?"

  #94 opened 5 years ago by kbuzzard
  0

• Sian Carey fellowship

  #91 opened 5 years ago by kbuzzard
  0

• Drop down menu for levels

  #87 opened 5 years ago by pglutz
  2

• explain implicit inputs

  #89 opened 5 years ago by kbuzzard
  0

• Advanced Proposition world: Level 1/10

  #88 opened 5 years ago by arademaker
  1

• Night Mode

  #62 opened 5 years ago by ericrbg
  4

• props aren't decidable in world 7

  #84 opened 5 years ago by kbuzzard
  0

• Save progress

  #73 opened 5 years ago by rudolfovic
  7

• it's hard to find this repository

  #60 opened 5 years ago by robx
  3

• nat versus mynat issue with literal zeros

  #74 opened 5 years ago by gjm11
  2

• not_succ_le_self better solution

  #71 opened 5 years ago by kbuzzard
  1

• add odd and even numbers

  #80 opened 5 years ago by kbuzzard
  0

• Description ahead of `succ_inj'`

  #68 opened 5 years ago by stanescuUW
  1

• hacker news UX comments

  #64 opened 5 years ago by kbuzzard
  1

• \l and \1

  #61 opened 5 years ago by kbuzzard
  1

• basic tactics file

  #57 opened 5 years ago by kbuzzard
  1

• add basic stuff about primes

  #81 opened 5 years ago by kbuzzard
  0

• Advanced Addition World, Level 11: add_right_eq_zero

  #76 opened 5 years ago by trj2059
  1

• "unknown identifier 'not_iff_imp_false'" error in Advanced Proposition Level 9

  #65 opened 5 years ago by edderiofer
  3

• Advanced muit world level 4 revert

  #63 opened 5 years ago by kbuzzard
  2

• eq_zero_of_add_right_eq_self

  #78 opened 5 years ago by kbuzzard
  1

• Lean can get stuck an infinite loop

  #67 opened 5 years ago by FreeFull
  1