info view ineraction

Stream: general

[Matthew Pocock]

I find myself highlighting sub-expressions in the infoview. It would be kind of neat if when I do that and hover, the IDE ran a bunch of standard tactics (exact, assumption, ...) and if those happen to solve that fragment, gives me the option to import that into my in-progress proof. Extra credit if it will synthesise the skeleton of an intro or apply or case block.

[Patrick Massot]

All this is coming.

[Patrick Massot]

But we have infrastructure issues currently which prevents updating the ProofWidgets library in Mathlib.