What is a parent structure?

Stream: general

[Chris Hughes]

Why doesn't this work

import ring_theory.algebra

structure alg_equiv (α β γ : Type*) [comm_ring α] [ring β] [ring γ]
  [algebra α β] [algebra α γ] extends @alg_hom α β γ _ _ _ _ _ :=
--invalid 'structure', expression must be a 'parent' structure

[Kevin Buzzard]

That's a bit annoying isn't it! My impression is that Lean chokes on the @ symbol and doesn't go any further.

structure foo (α : Type) :=
(hello_mum : ℕ)

structure bar (α : Type) extends @foo α := -- same error
(hello_world : bool)

[Kevin Buzzard]

You could of course just work around it by putting the fields in and making the projection yourself. Are there any serious disadvantages to this other than it being a bore?

[Chris Hughes]

I think the best solution is to make that field of alg_hom explicit. Then using the notation should work

[Chris Hughes]

#1296

[Kevin Buzzard]

6^4