Zulip Chat Archive

Stream: general

Topic: What is a parent structure?


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Chris Hughes (Aug 03 2019 at 19:16):

#1296

view this post on Zulip Kevin Buzzard (Aug 03 2019 at 22:05):

6^4


Last updated: May 12 2021 at 23:13 UTC