Zulip Chat Archive

Stream: general

Topic: fin ops and unsigned ops in core


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 27 2021 at 03:12):

Are they overridden by the VM?

view this post on Zulip Yakov Pechersky (Jan 27 2021 at 04:32):

Not as far as I can tell, nothing in the files would suggest so

view this post on Zulip Johan Commelin (Jan 27 2021 at 04:33):

I guess you can only find out by looking at the C++

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 01 2021 at 01:43):

lean#525

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Feb 02 2021 at 18:15):

Attempt number two: lean#527


Last updated: May 13 2021 at 06:15 UTC