Commit 2023-06-29 02:25 976c41ef

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 *.