Commit 2019-07-29 16:17 363f1873
View on Github →feat(tactic/extract_goal): create stand-alone examples out of current goal (#1233)
- feat(tactic/extract_example): create stand-alone examples out of current goal
- feat(tactic/extract_example): add formatting and options
- feat(tactic/extract_goal): rename to
extract_goal - Update src/tactic/interactive.lean Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com
- make instances anonymous when the name starts with
_ - add doc strings
- feat(tactic/interactive): exact_goal works on defs