Zulip Chat Archive
Stream: mathlib4
Topic: lift
Johan Commelin (Sep 19 2022 at 10:34):
I would like to start working on porting lift.
Reid Barton (Sep 20 2022 at 07:55):
@Floris van Doorn Do you remember if there was a specific reason not to make the cond field of can_lift an out param?
Floris van Doorn (Sep 20 2022 at 08:24):
I didn't really consider it. I tried it as a field, and it worked well enough.
I have no objection against changing it.
Johan Commelin (Sep 20 2022 at 13:52):
Here's a PR that slightly refactors lift in mathlib3.
refactor(tactic/lift): remove attribute/simp-set and swap side goal #16565
Ruben Van de Velde (Dec 22 2022 at 21:14):
Any news on lift? Data.Rat.Lemmas uses it
Scott Morrison (Dec 22 2022 at 22:02):
https://github.com/leanprover-community/mathlib4/pull/723 has been waiting for review/refactor for a long time, sorry
Last updated: Dec 20 2023 at 11:08 UTC