Scientific literals for Pi types

Stream: Is there code for X?

[Eric Wieser]

Am I right in thinking the following is missing? Should we have it?

instance Pi.instOfScientific {ι : Type*} {α : ι → Type*} [∀ i, OfScientific (α i)] : OfScientific (Π i, α i) where
  ofScientific m s e := fun _ => OfScientific.ofScientific m s e

@[simp]
theorem Pi.ofScientific_apply {ι : Type*} {α : ι → Type*} [∀ i, OfScientific (α i)] (m : Nat) (s : Bool) (e : Nat) (i : ι) :
    (OfScientific.ofScientific m s e : Π i, α i) i = OfScientific.ofScientific m s e :=
  rfl

[Eric Wieser]

With motivation:

-- already works
#check (3 : Fin 3 → ℚ)
#check (3 : Fin 3 → ℝ)

-- needs this instance
#check (3.7 : Fin 3 → ℚ)
#check (3.7 : Fin 3 → ℝ)