Zulip Chat Archive
Stream: general
Topic: fin ops and unsigned ops in core
Yakov Pechersky (Jan 26 2021 at 19:20):
Is there a reason why init/data/fin/ops and 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: Dec 20 2023 at 11:08 UTC