mathlib4
mathlib4 copied to clipboard
copy lean3port/ported into mathlib4
trafficstars
https://github.com/leanprover-community/lean3port/compare/ported
And make mathlib prelude-fre
is this closed as completed or no longer necessary? And if completed, what were the changes?
Closed as completed. AFAICT we've already ported the relevant files from core.