## Stream: new members

### Topic: defining a class

#### Heather Macbeth (Jul 18 2020 at 23:30):

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.

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.

#### Adam Topaz (Jul 19 2020 at 00:36):

Presumably h.seven would work if you use (h : sevenish G) instead of [...]

#### Adam Topaz (Jul 19 2020 at 01:30):

scratch that. h.seven doesn't work even if you use (h : ...).

#### Notification Bot (Jul 19 2020 at 05:03):

This topic was moved by Scott Morrison to #general > defining a class

Last updated: May 12 2021 at 05:19 UTC