[Merged by Bors] - feat(library/init/coe): backport has_coe_to_sort/has_coe_to_fun from Lean 4

[urkud]

No description provided.

[gebner]

bors try

[bors]

try

Build failed:

• Build macos Debug

[eric-wieser]

bors try

[bors]

try

Build failed:

• Build linux Release

[urkud]

bors try

[bors]

try

Build succeeded:

• Build linux Release
• Build macos Release
• Build emscripten
• Build windows Release
• Build linux Debug
• Build macos Debug
• Build sanitized

[urkud]

The following example fails with the new has_coe_to_sort:

universe u

instance {α : Type u} : has_coe_to_sort (set α) (Type u) := ⟨λ s, {x // x ∈ s}⟩

example : ↥({0} : set ℕ) := ⟨0, rfl⟩

Error: "5:29: invalid constructor ⟨...⟩, 'has_coe_to_sort.coe' is not an inductive type"

I have no idea why this happens.

[bryangingechen]

bors try

[bors]

try

Build succeeded:

• Build macos Release
• Build linux Debug
• Build macos Debug
• Build emscripten
• Build linux Release
• Build windows Release
• Build sanitized

[eric-wieser]

What's the status of this PR?

[gebner]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build emscripten
• Build linux Debug
• Build linux Release
• Build macos Debug
• Build macos Release
• Build sanitized
• Build windows Release