Constructor for extended structure

Stream: new members

[Nicolò Cavalleri]

Is there a way of doing this:

variables (α : Type*) (β : Type*) (γ : Type*) (δ : Type*)

structure foo :=
(to_fun    : α → β)
(g         : γ)

structure bar :=
(to_fun    : α → β)
(d         : δ)

set_option old_structure_cmd true

structure foobar extends foo α β γ, bar α β δ

def the_foobar (a : foo α β γ) (d : δ) : foobar α β γ δ := ⟨a, d⟩

without doing this:

variables (α : Type*) (β : Type*) (γ : Type*) (δ : Type*)

structure foo :=
(to_fun    : α → β)
(g         : γ)

structure bar :=
(to_fun    : α → β)
(d         : δ)

set_option old_structure_cmd true

structure foobar extends foo α β γ, bar α β δ

def the_foobar (a : foo α β γ) (d : δ) : foobar α β γ δ := ⟨a.to_fun, a.g, d⟩

?

[Eric Rodriguez]

def the_foobar (a : foo α β γ) (d : δ) : foobar α β γ δ := {d:=d, ..a} is the best I know, not sure if it works with anonymous constructors

[Eric Rodriguez]

you can even do things like def the_foobar (a : foo α β γ) (d : bar α β δ) : foobar α β γ δ := {..d, ..a}

[Nicolò Cavalleri]

Ok thanks right I don't know why that did not come to my mind...