mathlib
197b5015 - feat(tactic/extract_goal): better support for `let` expressions (#3496)

Commit

6 years ago

feat(tactic/extract_goal): better support for `let` expressions (#3496) Improve treatment of let expressions #3375 Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author

cipher1024

Parents

64335dec

mathlib 197b5015 - feat(tactic/extract_goal): better support for `let` expressions (#3496)

mathlib
197b5015 - feat(tactic/extract_goal): better support for `let` expressions (#3496)