old_structure_cmd cannot extend structures with subobjects

[kckennylau]

class A : Type :=
(B : true)

class C extends A :=
(D : true)

set_option old_structure_cmd true
class E extends C :=
(F : true)

#print E
/-
@[class]
inductive E : Type
constructors:
E.mk : Π [_to_A : A], true → true → E
-/

def G : E :=
{ B := trivial,
  D := trivial,
  F := trivial }
/-
invalid structure value {...}, expected type is known, but it is not a structure
  E
-/

[kckennylau]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/not.20a.20structure

[gebner]

WTF?

BTW, this doesn't work either:

structure X : Type
#check { X . }
-- invalid structure instance, 'X' is not the name of a structure type

[gebner]

This doesn't work either:

set_option old_structure_cmd true
class A (α : Type).
class B (α : Type) extends A α :=
(BB : ℕ)
class C (α : Type) [A α].
class D (α : Type) extends B α, C α.