Commit 2023-01-04 18:33 047e52ab
View on Github →feat: port Data.Bundle (#1288) Not sure what to do with:
set_option quotPrecheck false in
/-- The canonical projection defining a bundle. -/
scoped notation "π" => @Bundle.TotalSpace.proj _
But otherwise what seems like a fairly straightforward port.