Issues
- 1
Don't show locked items in inventory.
#265 opened by miguelmarco - 3
Building issue
#263 opened by kant2002 - 1
`have` a hypothesis that has multiple premises
#264 opened by Qinggao1729 - 1
Delete tmp games
#255 opened by joneugster - 3
Can't write "use (succ(succ a))"
#258 opened by VasiliPupkin256 - 0
fix filtering of "unsolved goal" error
#257 opened by joneugster - 1
- 4
Struggling to run games locally manually
#254 opened by ndcroos - 11
Question: Can you have `calc` blocks in games?
#223 opened by lnay - 4
Does this game have hints for new beginner ?
#252 opened by geraltgod - 2
Ask question on Zulip
#227 opened by joneugster - 2
- 2
Robo Anonyme Funktionen 1 crash
#249 opened by NoLongerBreathedIn - 5
feat: user feedback
#218 opened by joneugster - 10
Adding Image to the left side pane of a world
#235 opened by JadAbouHawili - 1
(Support changing abbreviation letter) Support writing math symbols using ; in addition to \
#225 opened by JadAbouHawili - 1
- 1
feat: inventory of cheat sheets/summaries in addition to tactics, definitions and theorems
#246 opened by TentativeConvert - 0
- 2
Update to Lean v4.8
#243 opened by MithicSpirit - 3
Competition
#242 opened by swisstackle - 5
failed to execute `c++`
#241 opened by linonetwo - 1
Always show solutions after level completion
#240 opened by matthiasgeihs - 2
- 3
`lake exe i18n --export-json` does not support `#~`
#210 opened by JiechengZhao - 1
local notation in inventory
#216 opened by joneugster - 1
- 0
(some?) error messages appear twice
#209 opened by TentativeConvert - 1
forbidden keywords
#215 opened by joneugster - 2
feat: allow for custom translations
#237 opened by joneugster - 0
Level Introduction Auto-Scrolling
#230 opened by Trequetrum - 5
Information disappears and reappears in editor mode
#226 opened by kbuzzard - 0
- 1
Level 5 / 7 : Rewriting on the final world (World: Redux: ↔ World Tactics) on "A Lean Intro to Logic" and general feedback
#232 opened by awefhio - 0
Player proceeds after error
#233 opened by joneugster - 2
- 3
"A Lean Intro to Logic" server problem
#229 opened by Madjosz - 1
Hint shows blue squiggle
#211 opened by joneugster - 1
mark statement from last level
#214 opened by joneugster - 3
bug: stuck on unexpected end of input
#222 opened by bjarki781 - 3
remove flags from language selector
#208 opened by TentativeConvert - 0
Bug: Lost progress
#221 opened by joneugster - 1
- 2
- 0
feat: add bonus levels
#217 opened by joneugster - 3
- 0
proof statement with itself
#213 opened by joneugster - 7
Interface scrolls down, hiding the top
#202 opened by noamraph - 2
Error message "Cannot read properties of undefined (reading 'steps')" when loading "add_mul" level.
#200 opened by Laurens-Klijn - 2
`repeat` causes server crash
#201 opened by krtab