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: May 02 2025 at 03:31 UTC