Zulip Chat Archive

Stream: new members

Topic: structure value invalid


view this post on Zulip Yakov Pechersky (Mar 31 2021 at 01:41):

An unfamiliar error:

invalid structure value {...}, expected type is not known(solution: use qualified structure instance { struct_id . ... }

I don't think I can easily make a #mwe. This might have to do with clashing class names, I've defined my own group and am trying to say

def to_group (G : Type*) [group G] : _root_.group G :=
{ mul := group.op,
  mul_assoc := λ _ _ _, (group.assoc' _ _ _).symm,
  one := group.e,
  one_mul := group.e_op',
  mul_one := group.op_e',
  inv := group.inv,
  div := λ f g, group.op f (group.inv g),
  div_eq_mul_inv := λ _ _, rfl,
  mul_left_inv := group.inv_op' }

view this post on Zulip Julian Berman (Mar 31 2021 at 02:35):

Does it in fact work if you do what it says? -- i.e. { _root_.group G . mul := group.op, blabla }?

view this post on Zulip Julian Berman (Mar 31 2021 at 02:36):

I'm pretty sure I've seen that error before but I'm sure in much simpler poking than whatever you're up to


Last updated: May 16 2021 at 20:13 UTC