calc widget UX

Stream: general

[Miguel Marco]

About UX, I just started using the lightbulb to create a calc skeleton, and I noticed that it creates a single line proof, which is almost never what you will need (you use calc to chain several (in)equalities, afterall). Wouldn't it be better to start with more than one? Or even better: have another lightbulb to insert new lines in the proof.

[Ruben Van de Velde]

What happened to the calc widget?

[Miguel Marco]

I didn't know about it. How does it work?

[Eric Rodriguez]

I've also noticed the widget for calc but no clue how it works

[Patrick Massot]

It should write all instructions below the tactic state.

[Miguel Marco]

I just see a text saying "Please select subterms".

[Patrick Massot]

And this indeed exactly what you should do.

[Miguel Marco]

How? I try to select subterms in the infoview and nothing happens. If I do so in the lean file, the message disappears.

[Patrick Massot]

Maybe you misunderstand what select means in this context. You need to shift-click on sub terms in the current goal.

[Mario Carneiro]

probably it should say that, shift-clicking isn't something you normally do in lean

[Patrick Massot]

This is the normal way of selecting things in the info view. It had nothing to do with this widget and is provided by Lean core. But indeed we could say it in the message.

[Mario Carneiro]

Is there something else you can select in the infoview in this manner?

[Patrick Massot]

Sure. Many widgets use this feature.

[Mario Carneiro]

non-widgets

[Mario Carneiro]

or stock / builtin widgets

[Mario Carneiro]

interacting with the goal view and expected type view doesn't reveal anything shift-clickable

[Patrick Massot]

I don't think so. You can always select stuff, but then nothing happens if you have no import.

[Patrick Massot]

So again I agree we should make the message more beginner-friendly.

[Miguel Marco]

I see. It works as you say.

[Eric Rodriguez]

I also really struggled to understand exactly how it was meant to be used; I see now that you place your start and end goal and then place your cursor somewhere on the by, then allowing you to select this. Also not super easy to figure out.

[Eric Rodriguez]

I think some more documentation would be super welcome

[Kim Morrison]

shift-click should be in the message

[Geoffrey Irving]

We may want to move the calc discussion to a different thread.

[Notification Bot]

23 messages were moved here from #general > "Missing Tactics" list by Timo Carlin-Burns.