Default `OfScientific` instance

Stream: mathlib4

[Heather Macbeth]

I'd like to make Rat the default OfScientific instance in mathlib, overriding Float which is the default instance in core. So something like 1.7 without a type annotation would be interpreted as Rat.

@Gabriel Ebner told me that this should be an easy change, just put a line somewhere making that the default instance and perhaps giving it a higher priority than the Float one in core, so that it takes precedence. But what is the right place in mathlib to put this?

[Thomas Murrills]

Maybe Mathlib.Init.Data.Rat.Basic? (Data.Rat.Basic is where the Rat instance for OfScientific is in std4, and Mathlib.Init.Data.Rat.Basic already imports Std.Data.Rat.Basic, as you'd expect)

[Yaël Dillies]

That's a leftover file from Lean 3's architecture, though. Not sure we want to mess with that.

[Thomas Murrills]

Oh, I thought that it was named “Init” because it’s imported by every Mathlib file, sort of like a prelude. Does Mathlib have anything prelude-like?

[Yaël Dillies]

Std is prelude-like to mathlib4, but that doesn't really help here, no.

[Scott Morrison]

How about Mathlib.Data.Rat.Init? That is where we set up the notation for ℚ, and it is the earliest place where have Std.Data.Rat imported.