Zulip Chat Archive
Stream: new members
Topic: has_coe_t vs has_coe
Eric Wieser (Jul 30 2020 at 10:17):
What's the difference between docs#has_coe_t and docs#has_coe?
Eric Wieser (Jul 30 2020 at 10:17):
The docs say only
Auxiliary class that contains the transitive closure of has_coe.
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?
Alex J. Best (Jul 30 2020 at 18:36):
Does https://leanprover-community.github.io/mathlib_docs/notes.html#use%20has_coe_t help?
Alex J. Best (Jul 30 2020 at 18:37):
and https://leanprover-community.github.io/mathlib_docs/notes.html#coercion%20into%20rings
Eric Wieser (Jul 30 2020 at 19:54):
Yes, that does
Eric Wieser (Jul 30 2020 at 19:55):
It would be great if has_coe_t could link to one or both of those
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.
Eric Wieser (Jul 30 2020 at 21:06):
Oh, I missed that. Can mathlib override the docstring with a command?
Last updated: Dec 20 2023 at 11:08 UTC