coercion from PNat to Rat

Stream: mathlib4

[David Renshaw]

Lean 3:

import data.pnat.basic
import data.rat.basic

def foo (x : ℕ+) : ℚ := x
#print foo
-- λ (x : ℕ+), ↑x

Lean 4:

import Mathlib.Data.PNat.Basic
import Mathlib.Data.Rat.Basic

def foo (x : ℕ+) : ℚ := x

#print foo
-- fun x => ↑↑x

The Lean 4 versions has two up arrows, while the Lean 3 version only has one.
Is that expected?

[Mario Carneiro]

yes

[Mario Carneiro]

the lean 3 version was undesirable and if you use simp on it you will see it change to two arrows

[David Renshaw]

why was the Lean 4 version not backported to Lean 3?

[Kevin Buzzard]

The answer might be "coercions changed in core"