Lean.ToExpr Int

Stream: lean4

[Eric Wieser]

We have three instances for Lean.ToExpr Int:

• docs#Mathlib.instToExprInt_mathlib and docs#instToExprInt_qq; toExpr (-1) = q(Int.negSucc 0)
• docs#Lean.instToExprInt: toExpr (-1) = q(-1)

Does anyone remember the history here? The mathlib one looks like an accident since it's autogenerated, and the Qq one looks like it might predate the instance being in core, but perhaps there is a connection to the "raw cast" stuff used by norm_num etc.

[Floris van Doorn]

I (or loogle) cannot find the qq one.

[Eric Wieser]

I deleted it yesterday in https://github.com/leanprover-community/quote4/pull/58

[Floris van Doorn]

There are more clashes

[Floris van Doorn]

@loogle Lean.ToExpr Lean.BinderInfo

[loogle]

:search: Mathlib.instToExprBinderInfo_mathlib, instToExprBinderInfo_qq

[Eric Wieser]

I suspect all the clashes at least are defeq to each other

[Eric Wieser]

Eric Wieser said:

I deleted it yesterday in https://github.com/leanprover-community/quote4/pull/58

My thinking here was that mathlib almost certainly has nowhere that depends on the qq instance that doesn't already import that mathlib one. If we removed the mathlib one first, we wouldn't be able to notice the effect until we also removed the qq one. Doing it the other way around makes the CI situation simpler.

[Floris van Doorn]

Yeah, that's likely. I don't know the history for the ToExpr distinction. I think it's good to try to delete the Mathlib one, and merge it if everything builds.

[Kyle Miller]

The Int.negSucc 0 interpretation is breaking nightly-testing, since #eval now can try using ToExpr instances to pretty print results. I'll delete the mathlib one too, unless you've already gotten to it @Eric Wieser

[Eric Wieser]

Please do, I didn't get around to it

[Kyle Miller]

#17590