Zulip Chat Archive
Stream: new members
Topic: Unfolding has_zero
Eric Wieser (Jul 21 2020 at 18:03):
How do I replace (0 : T) with the struct associated with the zero member of has_zero T?
Eric Wieser (Jul 21 2020 at 18:07):
Solved with unfold has_zero.zero.
Kevin Buzzard (Jul 21 2020 at 18:08):
Yeah 0 is just notation for has_zero.zero
Last updated: Dec 20 2023 at 11:08 UTC