Yakov Pechersky (Jan 26 2021 at 19:20):
Is there a reason why
init/data/unsigned/ops are in core and not in mathlib? As far as I've found, nothing in core seems to import those.
Bryan Gin-ge Chen (Jan 26 2021 at 19:24):
Probably just historical reasons. I think PRs removing them from core and adding them to mathlib would probably be accepted.
Mario Carneiro (Jan 27 2021 at 03:12):
Are they overridden by the VM?
Yakov Pechersky (Jan 27 2021 at 04:32):
Not as far as I can tell, nothing in the files would suggest so
Johan Commelin (Jan 27 2021 at 04:33):
I guess you can only find out by looking at the C++
Johan Commelin (Jan 27 2021 at 04:34):
there is some list somewhere that lists all the lean declarations that core expects to be in core... but I forgot where to find that list
Yakov Pechersky (Feb 01 2021 at 01:43):
Yakov Pechersky (Feb 01 2021 at 02:43):
As I thought,
vector relies heavily on
fin, and doc-gen didn't properly flag the dependencies on
fin/ops, so this won't work without a much larger refactor.
Yakov Pechersky (Feb 02 2021 at 18:15):
Attempt number two: lean#527
Last updated: May 13 2021 at 06:15 UTC