Zulip Chat Archive

Stream: general

Topic: Where is `has_coe_to_sort (subalgebra R A)`?

Eric Wieser (Nov 17 2020 at 15:41):

I've found myself using subalgebra in the past, but was surprised to find that the docs don't reveal any has_coe_to_sort instance! Is there an easy way to ask lean how it found the instance?

Kevin Buzzard (Nov 17 2020 at 15:57):

One can start investigating this sort of thing like this:

import algebra.algebra.subalgebra

example (R : Type*) (A : Type*) [comm_semiring R]
  [semiring A] [algebra R A] : false :=
  let ZZZ : has_coe_to_sort (subalgebra R A) := by apply_instance,

Kevin Buzzard (Nov 17 2020 at 15:58):

The infoview says that ZZZ := coe_sort_trans and clicking on that tells us that submodule.has_coe_to_sort exists and etc. Is this enough clues?

Eric Wieser (Nov 17 2020 at 16:08):

docs#coe_sort_trans is almost certainly what I wanted to find, thanks!

Eric Wieser (Nov 17 2020 at 16:08):

And using let sounds like a good trick to remember.

Last updated: Dec 20 2023 at 11:08 UTC