## Stream: new members

### Topic: structure value invalid

#### 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' }


#### 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 }?

#### 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