Zulip Chat Archive

Stream: general

Topic: equality function (bool)


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Hunter Freyer (Sep 21 2020 at 21:11):

yaaaay. It's so obvious when one is told how to do it :P

view this post on Zulip 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 to_bool live?

view this post on Zulip 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.

On zulip, we can also do this: docs#to_bool or src#to_bool

view this post on Zulip Hunter Freyer (Sep 21 2020 at 21:15):

womp womp, 404

view this post on Zulip Bryan Gin-ge Chen (Sep 21 2020 at 21:17):

This works: docs#decidable.to_bool / src#decidable.to_bool

view this post on Zulip Hunter Freyer (Sep 21 2020 at 21:17):

rad. Thanks for the help!


Last updated: May 12 2021 at 22:15 UTC