Aggressiveness of nat literal conversion

Stream: mathlib4

[Chris B]

I encountered this behavior earlier and found it surprising. This does appear to be the same behavior as what was in mathlib3, but I'm curious whether there's any desire to change it, or if I'm just thinking about this wrong:

-- #eval x = 2
def x : Fin 10 :=
  let a : Nat := 30 / 15
  a

-- #eval y = 0
def y : Fin 10 :=
  let a : Nat := 30
  let b : Nat := 15
  (a / b)

-- #eval z = 0
def z : Fin 10 := (30 / 15)

Particularly in y, I was expecting it to elaborate to OfNat ((a : Nat / b : Nat)) : Fin 10, instead of (OfNat a : Fin 10) / (OfNat b : Fin 10).

[Mario Carneiro]

This follows the usual rule of outside-in coercion, which means that you usually get ↑a / ↑b instead of ↑(a / b) when both are a possibility

[Mario Carneiro]

Another way to force the x behavior is

#eval show Fin 10 from (30 / 15 : Nat) -- 2

[Chris B]

Can you elaborate on the outside-in thing? Do you start at the outermost term and see what the inner-most possible way to do the conversion is?

[Sebastian Ullrich]

I think it's better described as outside-in elaboration. The expected type is propagated as far as possible, which pushes coercions towards the leaves.

[Chris B]

Got it, thanks.