automatic coercion?

Stream: general

[Kenny Lau]

import data.finset

#check λ s : finset ℕ, (s : set ℕ) -- invalid type ascription, term has type
#check λ s : finset ℕ, (↑s : set ℕ) -- λ (s : finset ℕ), ↑s : finset ℕ → set ℕ
#check λ x : ℕ, (x : ℤ) -- λ (x : ℕ), ↑x : ℕ → ℤ

[Kenny Lau]

why does N auto. coerce to Z but not finset to set?

[Shing Tak Lam]

(nevermind)

[Shing Tak Lam]

If I understand coe correctly, Lean will coerce the first one if it has_coe, the second one if it has_lift. There is

@[priority 10] instance cast_coe : has_coe ℕ α := ⟨nat.cast⟩

So the Nat to Int coercion works. But in data.finset, there's has_lift (finset α) (set α) but not has_coe (finset α) (set α), so the first one doesn't work.

[Gabriel Ebner]

Note that cast_coe has changed recently, it is now has_coe_t. But that doesn't have an effect on the finset coercion, which is exactly how @Shing Tak Lam described it.

@[priority 900] instance cast_coe : has_coe_t ℕ α := ⟨nat.cast⟩

[Shing Tak Lam]

(The folder I'm working in is on Lean 3.8.0, which is why I still have the old cast_coe)

[Kenny Lau]

why do we have such a distinction?