Zulip Chat Archive

Stream: general

Topic: refine_struct doesn't work with module


view this post on Zulip Scott Morrison (Aug 16 2020 at 08:33):

It seems refine_struct doesn't work with module.

import algebra.module.basic

example {α β : Type} [ring α] [add_comm_group β] : module α β :=
begin
  refine_struct { .. },
end

(says too many constructors).

view this post on Zulip Scott Morrison (Aug 16 2020 at 08:34):

@Simon Hudon, any ideas?

view this post on Zulip Simon Hudon (Aug 16 2020 at 14:47):

Let's see

view this post on Zulip Simon Hudon (Aug 16 2020 at 14:58):

Ok, I have a fix. It's because module is not a structure itself so I need to use whnf before getting the structure name

view this post on Zulip Simon Hudon (Aug 16 2020 at 15:08):

#3828


Last updated: May 15 2021 at 23:13 UTC