Zulip Chat Archive
Stream: general
Topic: construct destruct
Matthew Ballard (Aug 10 2023 at 12:38):
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 (Aug 10 2023 at 12:40):
That's "structure eta" (c.f docs#Prod.mk.eta)
Matthew Ballard (Aug 10 2023 at 14:03):
So there is nothing like docs#Simps.headStructureEtaReduce in core?
Kyle Miller (Aug 10 2023 at 14:08):
#5717 provides the eta_struct
tactic, but it hasn't been merged yet
Matthew Ballard (Aug 10 2023 at 14:09):
Oh that is nice. So I guess the implicit answer is no?
Kyle Miller (Aug 10 2023 at 14:10):
Yeah, that's my understanding, other than manually doing change
somewhere and relying on eta for structures being a definitional equality
Last updated: Dec 20 2023 at 11:08 UTC