Zulip Chat Archive

I seem to have set up a class in a bad way, or perhaps am using it in the wrong way. I cannot get access to the information in the class hypothesis without an extra-line workaround. Toy example (error is "invalid field notation, function 'sevenish.seven' does not have explicit argument with type (sevenish ...)":

import algebra.group_power

class sevenish (G : Type*) [group G] : Prop :=
(seven : ∀ (g : G), g ^ 7 = 1)

example (G : Type*) [group G] [h : sevenish G] (g : G) : g ^ 14 = 1 :=
begin
  have h1 := h.seven g,
  -- error
end

example (G : Type*) [group G] [h : sevenish G] (g : G) : g ^ 14 = 1 :=
begin
  have h1 := h.seven,
  have h2 := h1 g,
  -- works, can continue with the hypothesis `g ^ 7 = 1`
end

Here is the real example, btw.

Adam Topaz (Jul 18 2020 at 23:51):

I think sevenish.seven g should work if you don't name the instance with h.

Adam Topaz (Jul 18 2020 at 23:51):

But I'm not near a computer.

Heather Macbeth (Jul 19 2020 at 00:08):

Yes, thank you!

Bryan Gin-ge Chen (Jul 19 2020 at 00:09):

I'm surprised that h.seven doesn't work.

Adam Topaz (Jul 19 2020 at 00:15):

There's some protection around fields of instances right? For example, you can see what happens when you try to do cases h. I wonder if this is why it doesn't work.