Zulip Chat Archive
Stream: mathlib4
Topic: Logic for `ULift` lemmas
Arien Malec (Nov 24 2022 at 04:00):
we have ULift/PLift lemmas spread across Control.ULift and Data.ULift.
Maybe there some deep logic for what lemmas go in what places, but perhaps this is a path dependency for how things were done in mathlib?
Scott Morrison (Nov 24 2022 at 15:08):
Yeah, mathlib is not always as organised as we might wish.
Last updated: Dec 20 2023 at 11:08 UTC