Point and click interface

[miguelmarco]

Would it be possible to have some kind of mouse interaction for typical basic operations? I mean actions such as:

• separate a goal that is a conjuction (that is, call fconstructor)
• separate a hypothesis that is a conjunction (that is, call choose or cases')
• Create two goals from a hypothesis that is a disjunction (that is, call cases)
• introduce the first part of a goal that is an implication (intro)
• introduce arbitrary objects for a goal that is of the form ∀ x,... (again intro)
• choose the corresponding objects from a hypothesis of the form ∃ x, ... (choose`).

There are other situations where this kind of approach could be used, but I just listed the most evident ones.

I am thinking on something like this: if you have a situation like the ones before, you can right-click on the corresponding part, and a menu shows up proposing the corresponding action (maybe with some fields to fill with the names of the hypothesis/objects that will appear), and a button to trigger the action. When the button is pressed, the corresponding tactic is written and executed.

The rationale for this request is that these are actions that are repeated a lot, and writing them once and again ends up being very boring. Also, maybe this approach could encourage users to explore the proof status with more attention (or maybe not).

[joneugster]

I am happy consider and merge contributions in this direction, but this is unfortunately out-of-scope for myself to work on

[tautastic]

@joneugster I'm currently working on it but not sure how far I'll get

[joneugster]

Cool! You should consider using the dev branch as base! It currently lacks a functioning editor, but I'll add that over the next days but I'd like to get a new version from these efforts and a LOT if not almost all code has been moved around

[tautastic]

@joneugster I was working on another issue and noticed that fixing it on main would probably result in merge conflicts later on. I would like to help as much as I can on getting the dev branch running. If you want to delegate any work just create an issue and tag me in it. I will definitely take a look and see what I can do :)

[PatrickMassot]

@tautastic are you aware of the suggestion widget in Verbose Lean? You can see it in action in some gif in https://github.com/PatrickMassot/verbose-lean4/blob/master/README.md. The context is different, it uses the widget framework, but you could still take inspiration from that.

[tautastic]

@PatrickMassot Wow, this looks awesome, I will definitely check out the library.