Function coercion

Stream: new members

[Vasily Ilin]

There does not seem such a coercion but why not? Even more weird, a function from A to \N cannot be coerced to a function from A to \R! I don't understand why not.

variable (f : Ω → ℕ) (w : Ω)
#check (f w : ℝ) -- works
#check (f : Ω → ℝ) -- does not work

[Eric Wieser]

Automatic coercion of everything that might be useful isn't necessarily a good idea

[Vasily Ilin]

In math we usually don't even distinguish between mapping into naturals and reals, or between mapping into X and Y where X is a subtype of Y. So why not have this coercion in Lean?

[Yaël Dillies]

Because it might produce poor performance and unexpected results.

[Kyle Miller]

If you want to know how to do this coercion manually, usually you'll see something like this:

#check (fun x => f x : Ω → ℝ)

or this

#check ((↑) ∘ f : Ω → ℝ)

[Vasily Ilin]

Ohhh, wrapping it in a lambda expression, I see! What about a SimpleFunc?