Commit 2023-10-05 03:08 1bacc4ee

View on Github →

feat: Select and insert widgets (#7260) Builds a framework to define widgets allowing users to select some sub-expressions of the main goal to generate a tactic call. Four examples using this framework are included, generating calls to tactics conv, congrm and gcongr and generating new calc steps. Also includes a calc tactic code action to start a calc proof.

Estimated changes