Commit 2019-08-21 01:39 80700498
View on Github →feat(tactic/lift): add lift tactic (#1315)
- start on lift_to tactic
- finish lift tactic
- add instance to lift rat to int this required me to move some lemmas from rat/order to rat/basic which had nothing to do with the order on rat
- move test to test/tactic.lean
- add header and documentation
- add more/better documentation
- typo
- more documentation
- rewrite, minor
- move import
- remove can_lift attribute now we automatically construct the simp set used to simplify Thanks to @cipher1024 for the idea and writing the main part of this code
- remove occurrence of [can_lift]