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.