Basic expr functions

Stream: mathlib4

[Patrick Massot]

@Mario Carneiro is there any reason why https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Lean/Expr/Basic.lean is in mathlib rather than std? It contains stuff I'd like to use in a project not depending on mathlib. I know what you think: "what's the point of a project not depending on mathlib?". The answer is of course the hope to use it in mathlib some day.

[Floris van Doorn]

I think it's mostly added by mathlib4 contributors that noticed some basic function was missing (like me) and quickly needed one. I think they should eventually go to Std.

[Mario Carneiro]

@Patrick Massot Is there a reason? Yes, no one put it in std. I have been mostly reactive as an std maintainer, so if you want something to go in std you have to PR it yourself (or induce someone to PR it on your behalf).

I know what you think: "what's the point of a project not depending on mathlib?".

That's what you think, not me. Most of the mathematical projects I can imagine being involved with (including most of my mathlib contributions) could feasibly be done with very little mathlib, and I would like to make that more feasible, not less, and std is critical for that.

[Scott Morrison]

I thought it was me that could be accurately caricatured as believing that. :-) I agree we should move quite a lot to Std.

[Shreyas Srinivas]

Most of the mathematical projects I can imagine being involved with (including most of my mathlib contributions) could feasibly be done with very little mathlib, and I would like to make that more feasible, not less, and std is critical for that.

Which bits of mathlib will we eventually find in Std? For example, would it be things like basic data types, collections, and in general anything that an fpil person could use?

[Mario Carneiro]

more than that probably, but that sounds like a lower bound

[Mario Carneiro]

A fair number of general purpose tactics need to be moved as well

[Mario Carneiro]

stuff that makes lean generally easier to use and is not domain specific or tied to the mathlib class hierarchy could move to std

[Shreyas Srinivas]

Mario Carneiro said:

A fair number of general purpose tactics need to be moved as well

Thanks. I can imagine that many program/hardware verification tools wouldn't need mathlib if these things were available in std. Depending on what is being verified, mathlib would be an optional (and very useful) extra for such work.