Stream: new members
Topic: equality in lean
Vincent Siles (Oct 07 2019 at 11:34):
I was suprised to see I could define
def foo (b0: bool) (b1: bool) : bool := b0 = b1 directly. Looks like there is a type classe mechanism
decidable_eq behind that, am I right ?
Rob Lewis (Oct 07 2019 at 11:38):
Indeed. You can see how that gets elaborated with
set_option pp.implicit true #print foo
Vincent Siles (Oct 07 2019 at 11:41):
Thank you !
Last updated: May 13 2021 at 06:15 UTC