printing rationals

Stream: mathlib4

[Floris van Doorn]

In #29193 @Kim Morrison added a simple ToExpr Rat instance.
Unfortunately this instance is used for printing #eval expressions:

import Mathlib.Lean.Expr.Rat

#eval (12 : Rat) / 15 -- mkRat 4 5
-- remove the import to get (4 : Rat)/5

Can we get a better implementation of ToExpr Rat so that we pretty-print rational evaluation more nicely?
An option that seems to work was given by @Aaron Liu here: #Is there code for X? > Lean.ToExpr Rat @ 💬

[Kenny Lau]

that seems weird, you don't see 100 being printed as nat_lit 100

[Kim Morrison]

I'm confused, why do we care about the ToExpr instance? That's just a fall-back, isn't it, for when Repr is missing. We should just define that.

[Aaron Liu]

no repr doesn't give you hover info

[Aaron Liu]

and also used by eval%

[Kim Morrison]

It looks like Leo just added in lean#10961 a nicer instance, so I think the solution is just to delete the Mathlib instance on nightly-testing.

[Geoffrey Irving]

I'm hitting this as well. For example, here's the first 50 terms of the Mandelbrot Böttcher series. I did the thing where I formalised it all before running any of the subcomputations, and it did work first try, but alas because of this it came out ugly. :):/

#[mkRat 1 1, mkRat (-1) 2, mkRat 1 8, mkRat (-1) 4, mkRat 15 128, mkRat 0 1, mkRat (-47) 1024, mkRat (-1) 16,
  mkRat 987 32768, mkRat 0 1, mkRat (-3673) 262144, mkRat 1 32, mkRat (-61029) 4194304, mkRat 0 1,
  mkRat (-689455) 33554432, mkRat (-21) 512, mkRat 59250963 2147483648, mkRat 0 1, mkRat (-164712949) 17179869184,
  mkRat 39 2048, mkRat (-2402805839) 274877906944, mkRat (-1) 64, mkRat (-4850812329) 2199023255552, mkRat 29 2048,
  mkRat (-18151141041) 70368744177664, mkRat 0 1, mkRat 3534139462275 562949953421312, mkRat (-1039) 131072,
  mkRat (-22045971176589) 9007199254740992, mkRat (-1) 256, mkRat (-750527255965871) 72057594037927936,
  mkRat (-4579) 524288, mkRat 54146872254247683 9223372036854775808, mkRat 0 1,
  mkRat (-155379776183158669) 73786976294838206464, mkRat 2851 1048576,
  mkRat (-6051993294029466699) 1180591620717411303424, mkRat (-1) 1024,
  mkRat 7704579806709870203 9444732965739290427392, mkRat 92051 16777216,
  mkRat (-403307733528668035403) 302231454903657293676544, mkRat 0 1,
  mkRat 1650116480759617184697 2417851639229258349412352, mkRat (-229813) 67108864,
  mkRat 36124726440442241978477 38685626227668133590597632, mkRat (-41) 4096,
  mkRat (-225851495844149964787753) 309485009821345068724781056, mkRat 564373 67108864,
  mkRat (-35761228458796476847725737) 19807040628566084398385987584, mkRat 0 1]

[Eric Wieser]

@loogle Lean.ToExpr Rat

[loogle]

:search: instToExprRat_mathlib

[Eric Wieser]

Huh, I was convinced we already had an instance that used division

[Floris van Doorn]

The Core Repr instance uses division.

[Floris van Doorn]

docs#instReprRat