## Stream: lean4

### Topic: Structure Extensions

#### François G. Dorais (Mar 16 2021 at 07:38):

First, I think it's really cool that this works as I expect it to:

structure Bar (α) where bar : α

structure Foo {α} (x : α) : Prop where foo : True

structure FooBar (α) extends Bar α, Foo bar

#print FooBar
/-
inductive FooBar.{u_1} : Sort u_1 → Sort (max 1 u_1)
constructors:
FooBar.mk : {α : Sort u_1} → (_toBar : Bar α) → Foo _toBar.bar → FooBar α
-/


However, I don't understand how to make this work:

protected theorem FooBar.eq {α} : ∀ (f g : FooBar α), f.bar = g.bar → f = g
| ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
/-
dependent elimination failed, stuck at auxiliary equation
{ toBar := _toBar✝, toFoo := _toFoo✝ }.toBar.1 = { toBar := _toBar✝¹, toFoo := _toFoo✝¹ }.toBar.1
-/


Is there a reason why this shouldn't work?

PS: I kind of wish this shorthand worked too but this one seems like more of a rabbit hole.

structure Foo {α} (x : α) : Prop where foo : True

structure FooBar (α) extends Foo bar where bar : α


#### Mario Carneiro (Mar 16 2021 at 08:20):

protected theorem FooBar.eq {α} : ∀ (f g : FooBar α), f.bar = g.bar → f = g
| ⟨⟨_⟩,_⟩, ⟨⟨_⟩,_⟩, rfl => rfl


works

#### François G. Dorais (Mar 16 2021 at 08:23):

Of course! I see the .1 was the hint in the error message... subtle! Thanks!

Last updated: May 18 2021 at 23:14 UTC