Zulip Chat Archive

Stream: general

Topic: data.fintype.basic

Scott Morrison (Oct 13 2022 at 13:36):

data.fintype.basic has become a giant grab bag of things mentioning fintype. Would anyone like to have a go at carving pieces off it?

That and logic.equiv.basic (much lower down in the hierarchy) are two of the more conspicuous bottlenecks in the import graph at the moment.

Floris van Doorn (Oct 13 2022 at 13:51):


Scott Morrison (Oct 18 2022 at 07:01):

I split file#logic/equiv/basic a bit in #17038.

Last updated: Aug 03 2023 at 10:10 UTC