Topic: What is a parent structure?
Chris Hughes (Aug 03 2019 at 18:50):
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 (Aug 03 2019 at 18:58):
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 (Aug 03 2019 at 18:59):
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 (Aug 03 2019 at 19:00):
I think the best solution is to make that field of
alg_hom explicit. Then using the notation should work
Chris Hughes (Aug 03 2019 at 19:16):
Kevin Buzzard (Aug 03 2019 at 22:05):
Last updated: Aug 03 2023 at 10:10 UTC