Field notation inheritance for classes.

Stream: general

[Juho Kupiainen]

How do I get something like this to work?

class AA (α : Type):=
(some_op : α → α → ℕ )

class BB (α : Type) extends AA α :=
(other_op : α → α → ℕ)
namespace BB
def caabb {α : Type} (bb : BB α) := λ x y : α, (bb.some_op y x) + (bb.other_op x y)
end BB

I'm trying to build this so that you can write

def asd {α : Type} (bb1 bb2 : BB α) := λ x y, (bb1.caabb x y) + (bb2.caabb x y)

It works if I replace the class keyword with a structure keyword.

[Reid Barton]

You probably want structure everywhere, not class?

[Juho Kupiainen]

But then I can't say some_op a1 a2

[Reid Barton]

Oh... you said that. But what you wrote for bb.other_op is wrong already, so I don't understand what you actually want

[Reid Barton]

Ask a better question :upside_down:

[Juho Kupiainen]

Right. Say AA also extends the monoid class.

[Floris van Doorn]

If you want to keep using classes, this works:

class AA (α : Type):=
(some_op : α → α → ℕ)

class BB (α : Type) extends AA α :=
(other_op : α → α → ℕ)

open AA
namespace BB
def caabb {α : Type} [bb : BB α] := λ x y : α, some_op y x + other_op x y
end BB

[Floris van Doorn]

You need to open AA (so that AA.some_op is abbreviated to some_op) or alternatively define the projecction some_op in another namespace.

[Reid Barton]

If you're using classes, then you probably don't want to be using the field projection notation at all

[Reid Barton]

At least in a simple example like this

[Reid Barton]

You can also remove the name bb :

[Floris van Doorn]

But if you want multiple BB instances on the same type, classes might not be the thing you want to use.
This example

def asd {α : Type} (bb1 bb2 : BB α) := λ x y, (bb1.caabb x y) + (bb2.caabb x y)

will be a pain with classes.

[Floris van Doorn]

When using structures, the user specifies which structure to use (so you often use projection notation), and with classes you ask Lean to find the instance (like how Lean will find add_group on the integers). If you have two group or BB instances on the same type, Lean will just pick one for you, and it's a little ugly to specify it yourself (you can do it, with something like @ccaabb _ bb2 x y)