search

leanprover-community / lean4game

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

In typwriter mode: EDIT instead of DELETE #122

Closed TentativeConvert closed 1 year ago

TentativeConvert commented 1 year ago

Sometimes, I discover that the tactic I used was only slightly off, e.g. I should have used rw [add_comm b c] instead of rw [add_comm]. In these cases, it would be nice to be able to go back and edit the tactic rather than rewrite it. I suggest changing the behaviour of the "Delete"-buttons slightly so that the command in the line with the button is not erased.

The label of the button is imprecise in any case (as we don't delete just one line but also everything after). If we change the label to "Retry", it won't conflict with the behaviour I describe. Even better would be "Retry from here", but that’s a bit too long, I guess.

joneugster commented 1 year ago

implemented as suggested: "Retry" and copying the first (i.e. where the button is pressed) deleted command into the typewriter input