mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

copy lean3port/ported into mathlib4

Open gebner opened this issue 3 years ago • 1 comments
trafficstars

https://github.com/leanprover-community/lean3port/compare/ported

gebner avatar Aug 25 '22 15:08 gebner

And make mathlib prelude-fre

gebner avatar Aug 25 '22 15:08 gebner

is this closed as completed or no longer necessary? And if completed, what were the changes?

digama0 avatar Jan 18 '23 06:01 digama0

Closed as completed. AFAICT we've already ported the relevant files from core.

gebner avatar Jan 18 '23 06:01 gebner