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):

lean#525

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