data

Stream: general

[Kenny Lau]

Can we refactor src/data? Currently it looks like "miscellaneous" to me

[Kenny Lau]

real -> analysis
N, Z, Q -> number theory
finset -> combinatorics

[Patrick Massot]

This is a very controversial topic.

[Anne Baanen]

polynomial, mv_polynomial -> algebra?

[Patrick Massot]

And also real numbers can't go to analysis if we keep that analysis depends on topology but not the other way around (because of metric spaces).

[Simon Hudon]

The other issue is that N, Z and finset are also relevant to programming

[Johan Commelin]

I think the idea was that data would contain a bunch of definitions. That's fine with me. But I'm happy with all the proofs moving elsewhere.

[Patrick Massot]

You know the distinction is not clear at all.

[Kevin Buzzard]

Principal ideal domain is a definition.

[Floris van Doorn]

I think of data as definitions of new (usually basic) types that are used in many areas of math.

[Johan Commelin]

... and programming. :wink:

[Johan Commelin]

One could argue that polynomial is already too advanced.

[Chris Hughes]

I'm happy for it to contain things that are actually used for programming and nothing else. Making clear which parts of the library people actually use for programming might be useful.

[Scott Morrison]

I think we should definitely move polynomial. It already depends on monoid_algebra which clearly doesn't belong in data.

[Scott Morrison]

I don't think we can keep up the pretence that "topology doesn't depend on analysis" forever. :-)

[Scott Morrison]

Maybe topology could have some subfolders (general? point_set?) that aren't allowed to depend on analysis.

[Bryan Gin-ge Chen]

I guess we should put rules like that in the module docs.

[Mario Carneiro]

What about a topology.basic folder?

[Mario Carneiro]

I'm not sure it would be a good idea for such a folder, designed to encode a dependency barrier, to have a topical name

[Mario Carneiro]

it seems pretty silly to suggest that area X of maths does not depend on area Y