equality function (bool)

Stream: general

[Hunter Freyer]

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]

@[derive decidable_eq]
inductive colours
| red
| blue
| green
#check to_bool (colours.red = colours.blue)
#eval to_bool (colours.red = colours.blue)

[Hunter Freyer]

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

[Hunter Freyer]

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?

[Bryan Gin-ge Chen]

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

[Hunter Freyer]

womp womp, 404

[Bryan Gin-ge Chen]

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

[Hunter Freyer]

rad. Thanks for the help!