lean4game
lean4game copied to clipboard
leanprover-community
Information disappears and reappears in editor mode
I just finished a level of NNG, and the message at the end said "here's a backwards way of doing this level". So I switched to editor mode to experiment
and typed in the first line of the proof in the message, and then the entire message disappeared because the goal was no longer solved. Would it be possible to somehow "minimise" messages which have been displayed but which no longer apply, and the user can choose to unminimise a previously-displayed message? I guess a workaround is to copy the entire message into a comment in the Lean window first.
Thanks for the suggestion! I never specifically done anything about messages in the editor mode, but I agree that would be useful.
In Typewriter, when you press "Retry", all deleted messages turn gray until the next command is entered. I imagine using this feature in editor mode too.
I wonder whether for this specific use case a better solution would be to phrase the final comment “Here’s a completely backwards proof: …” as a separate level that contains the suggested backward proof as a proof template.
I would hesitate to clutter the interface with various (un)minimization options. If the users tries five different proofs they will easily end up with very many minimized messages to choose from. In which order would you want these to be displayed? And how does the user know which message to unminimize unless they can still see at least part of that minimized message?
A compromise that I could imagine, and which would cover the scenario under discussion, is that the final message (the “outro” of the level) remains permanently visible once the level is completed. (But still, I think a separate level with a proof template would be the better solution.)
A compromise that I could imagine [...] is that the final message [...] remains permanently visible once the level is completed. [...]
This will be implemented in the next bigger update.