Zulip Chat Archive

Stream: new members

Topic: How to use ring_hom.to_algebra


view this post on Zulip Amelia Livingston (May 11 2020 at 22:15):

I must've missed something because this works here, but I can't work out what. I've tried changing the instance priority and the class.instance_max_depth.

import ring_theory.algebra

variables {R : Type*} {S : Type*}
  (r : R) (s : S) [comm_semiring R] [comm_semiring S] (f : R →+* S)

instance foo : algebra R S := f.to_algebra

#check r  s -- failed to synthesize type class instance for has_scalar R S

view this post on Zulip Reid Barton (May 11 2020 at 22:28):

foo depends on f, but there's no way to infer it

view this post on Zulip Reid Barton (May 11 2020 at 22:29):

Whereas in the example you linked to, there's no extra variable

view this post on Zulip Amelia Livingston (May 11 2020 at 22:33):

Awesome, thank you


Last updated: May 10 2021 at 17:39 UTC