Zulip Chat Archive

Stream: new members

Topic: Function coercion

Vasily Ilin (Nov 14 2023 at 04:28):

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 (Nov 14 2023 at 09:52):

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

Vasily Ilin (Nov 16 2023 at 07:01):

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 (Nov 16 2023 at 08:23):

Because it might produce poor performance and unexpected results.

Kyle Miller (Nov 16 2023 at 19:30):

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 (Nov 18 2023 at 07:27):

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

Last updated: Dec 20 2023 at 11:08 UTC