Topic: equality function (bool)
Hunter Freyer (Sep 21 2020 at 21:08):
Hey, this seems pretty basic, but if I have a straightforward inductive datatype, how do I test for equality of two values in a way that returns a boolean? After lots of looking, I finally found that you can use
@[derive decidable_eq] to come close, but it still seems like there's a bit of gymnastics to get it to a bool, so I suspect I'm not doing it right.
Alex J. Best (Sep 21 2020 at 21:09):
@[derive decidable_eq] inductive colours | red | blue | green #check to_bool (colours.red = colours.blue) #eval to_bool (colours.red = colours.blue)
Hunter Freyer (Sep 21 2020 at 21:11):
yaaaay. It's so obvious when one is told how to do it :P
Hunter Freyer (Sep 21 2020 at 21:12):
I couldn't find documentation that describes derive, and I'm also struggling to find source for the standard libraries. Like, where does
Bryan Gin-ge Chen (Sep 21 2020 at 21:14):
derive sadly doesn't have good documentation yet (see #3533). To find the source, VS Code and emacs both should have a "go to definition" feature that you can use.
Hunter Freyer (Sep 21 2020 at 21:15):
womp womp, 404
Bryan Gin-ge Chen (Sep 21 2020 at 21:17):
Hunter Freyer (Sep 21 2020 at 21:17):
rad. Thanks for the help!
Last updated: May 12 2021 at 22:15 UTC