Zulip Chat Archive

Stream: mathlib4

Topic: coercion from PNat to Rat


David Renshaw (Jan 27 2023 at 18:27):

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 (Jan 27 2023 at 18:43):

yes

Mario Carneiro (Jan 27 2023 at 18:43):

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

David Renshaw (Jan 27 2023 at 18:44):

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

Kevin Buzzard (Jan 27 2023 at 22:08):

The answer might be "coercions changed in core"


Last updated: Dec 20 2023 at 11:08 UTC