construct destruct

Stream: general

[Matthew Ballard]

Say I have

structure A where
 x : Nat

def a : A := sorry

What is name of

A.mk a.x = a

Both general and for Expr’s?

[Eric Wieser]

That's "structure eta" (c.f docs#Prod.mk.eta)

[Matthew Ballard]

So there is nothing like docs#Simps.headStructureEtaReduce in core?

[Kyle Miller]

#5717 provides the eta_struct tactic, but it hasn't been merged yet

[Matthew Ballard]

Oh that is nice. So I guess the implicit answer is no?

[Kyle Miller]

Yeah, that's my understanding, other than manually doing change somewhere and relying on eta for structures being a definitional equality