Zulip Chat Archive

Stream: new members

Topic: has_coe_t vs has_coe


view this post on Zulip Eric Wieser (Jul 30 2020 at 10:17):

What's the difference between docs#has_coe_t and docs#has_coe?

view this post on Zulip Eric Wieser (Jul 30 2020 at 10:17):

The docs say only

Auxiliary class that contains the transitive closure of has_coe.

view this post on Zulip Eric Wieser (Jul 30 2020 at 10:18):

When should i declare an instance of has_coe_t, and when should I declare an instance of has_coe?

view this post on Zulip Alex J. Best (Jul 30 2020 at 18:36):

Does https://leanprover-community.github.io/mathlib_docs/notes.html#use%20has_coe_t help?

view this post on Zulip Alex J. Best (Jul 30 2020 at 18:37):

and https://leanprover-community.github.io/mathlib_docs/notes.html#coercion%20into%20rings

view this post on Zulip Eric Wieser (Jul 30 2020 at 19:54):

Yes, that does

view this post on Zulip Eric Wieser (Jul 30 2020 at 19:55):

It would be great if has_coe_t could link to one or both of those

view this post on Zulip Alex J. Best (Jul 30 2020 at 20:15):

Yeah I guess the only reason it doesn't (yet) is that has_coe_t is in core and that library note is in mathlib.

view this post on Zulip Eric Wieser (Jul 30 2020 at 21:06):

Oh, I missed that. Can mathlib override the docstring with a command?


Last updated: May 14 2021 at 07:19 UTC