Commit 2023-06-29 02:25 976c41ef
View on Github →feat: extract_lets
tactic (#3897)
This tactic is for taking let
bindings in the local context and "intro-ing" these bindings. It is like a cases
tactic for let
bindings. It can be used like extract_lets x y at h
or extract_lets at h
using intros
-like identifier lists. It also supports extract_lets at *
.