leanprover-community/lean4game

Issues

• Issue with Induction in Level 1/5 in Addition World for Natural Number Game

  #198 opened 10 months ago
  1

• Bug: in natural number game, "The tactic 'induction' is not available in this game!" where it should be available

  #197 opened 10 months ago
  1

• bug: disable not imported theorems

  #196 opened 10 months ago
  0

• Dev Container npm/node issues

  #195 opened a year ago
  2

• Unlock things on "relaxed" rules

  #194 opened a year ago
  0

• Editor mode broken on mobile

  #193 opened a year ago
  0

• Weird font in infoview

  #192 opened a year ago
  3

• Can't use intended tactic in level 5/6 of Advanced Addition World

  #191 opened a year ago
  3

• Can't use intended tactic in level 9/10 of Advanced Multiplication World

  #190 opened a year ago
  1

• Some hints are duplicated in mobile layout

  #189 opened a year ago
  1

• Warnings for disabled theorems/tactics

  #188 opened a year ago
  2

• "unknown identifier" error message

  #187 opened a year ago
  0

• Routing & Cookies

  #183 opened a year ago
  2

• Error when publishing game

  #180 opened a year ago
  5

• Add i18n support to the game.

  #179 opened 9 months ago
  8

• Google search

  #178 opened a year ago
  1

• Games get stuck

  #177 opened a year ago
  5

• Unlocked tactics bug

  #176 opened a year ago
  3

• Bad info displayed from Lean

  #175 opened a year ago
  1

• Unhelpful hover text

  #174 opened a year ago
  1

• The following keyworda need whitelisting

  #173 opened a year ago
  0

• Add opt-in to store preferences

  #172 opened a year ago
  1

• LemmaDoc / NewLemma with Namespaces

  #171 opened a year ago
  3

• Support Enter as keyboard shortcut for Next

  #170 opened a year ago
  1

• NewHiddenTactic entered in inventory

  #169 opened a year ago
  2

• When should `Hints` be triggered?

  #165 opened a year ago
  10

• Support hosting games from different lean versions.

  #164 opened 7 months ago
  2

• Mobile support

  #163 opened a year ago
  0

• Broken chat in Editor Mode

  #162 opened 10 months ago
  1

• Server crashes when repeatedly opening previously opened questions

  #161 opened a year ago
  4

• Variable name in Hints with `clear`

  #160 opened 7 months ago
  1

• Tactics not ordered alphabetically on world overview page

  #158 opened a year ago
  1

• “Rules” selector not reset/out of sync when game is erased

  #157 opened a year ago
  0

• test dev container

  #156 opened a year ago
  4

• The server will report an error libc++abi when Initialize game

  #155 opened a year ago
  2

• Lean Server: Watchdog error: Error while running Lake: could not change directory to

  #154 opened a year ago
  2

• Is it possible to duplicate an assumption

  #152 opened a year ago
  1

• Editor Mode Setting Not Persistent

  #151 opened a year ago
  2

• Display Game Not Found Error.

  #150 opened a year ago
  0

• Update world and level count for NNG on the landing page

  #149 opened a year ago
  0

• Tell developers to run `lake build` and `npm install` on every update

  #148 opened a year ago
  4

• Latex Documentation

  #147 opened 7 months ago
  2

• Lean Server: Watchdog error

  #146 opened a year ago
  4

• Update Running Locally URL

  #145 opened a year ago
  4

• UI enhancements: The Theorem Buttons

  #144 opened a year ago
  2

• Move "Show more help!" button in mobile design

  #143 opened a year ago
  0

• Filter identical hints

  #142 opened a year ago
  2

• I guess I don't understand nth_rewrite

  #141 opened a year ago
  1

• solutions?

  #140 opened a year ago
  2

• Additional unexpected errors

  #138 opened a year ago
  3