search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
137 stars 25 forks source link

Question: Can you have `calc` blocks in games? #223

Open lnay opened 2 months ago

lnay commented 2 months ago

What is the status of using a calc block in a level? Is it possible right now (I couldn't find a way to, or see anything in docs)?

joneugster commented 2 months ago

You can state your proof as

Statement ... : ... = yada yada := by
  Template
    Hole
      calc .....

Which will force the user to stay in the "editor mode", i.e where they can freely type in a multi-line editor (there's one sentence about it here). There they can enter anything, even calc-blocks, but the user experience might be less guided.

It's not possible to use calc as a tactic in the "typewriter mode", i.e. where you enter one tactic at a time as you see e.g. in the NNG. In fact it does not support any multi-line tactics at all.

I can recommend using the trans tactic instead of calc, that usually works quite well. (i.e. make trans [the most complicated type in your calc block] and then got on simplifying both new equations.)

lnay commented 2 months ago

Thanks!

lnay commented 2 months ago

@AlexBrodbelt , useful note here on level design

joneugster commented 1 month ago

I'll reuse this issue for anything about calc blocks in games, as it does come up occationally.

Current state: It would require serious modifications to the "Typewriter interface" in order to support calc-blocks in a semi-reasonable way, and it's afaik not on anybody's TODO-list. However, if there is serious interest and somebody wants to work on it, this might be the right place to discuss further details.

AlexBrodbelt commented 1 month ago

I would be happy to work on this, what would I have to do?