default implementations of type class in hierarchy

Stream: general

[Bernd Losert]

Say I have the following:

class Foo (α : Type*) :=
(foo : nat)

class Bar (α : Type*) extends Foo α :=
(bar : nat)

I would like some kind of mechanism (a macro?) that will allow me to define an instance of Bar by just specifying bar and having it use that implementation for foo. In other others, I want to write

instance : Bar nat := { bar := 10 }

and have it automatically set foo := 10 as well. Is this possible?

[Jireh Loreaux]

IIRC, I think you can just add (to_Foo := default_def_here) to the declaration of the Bar class (syntax might be different in Lean 4, and it's also possible I've botched this entirely). Is that what you're looking for?

[Bernd Losert]

Let me try. I'm using Lean 3.

[Jireh Loreaux]

Oh, your capitalization threw me off.

[Bernd Losert]

Oh cool. You're right. Nice.

[Yaël Dillies]

class Bar (α : Type*) extends Foo α :=
(bar : nat)
(foo := bar)

[Bernd Losert]

Yep. For some reason, I was reluctant to try the obvious.

[Yaël Dillies]

What distinguishes new fields from new default values is whether you specify the type or not. For example, this throws an error:

class Bar (α : Type*) extends Foo α :=
(bar : nat)
(foo : nat := bar) -- `foo` is already a field of `Foo`

[Bernd Losert]

I see. Didn't know that.