equality in lean

Stream: new members

[Vincent Siles]

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]

Indeed. You can see how that gets elaborated with

set_option pp.implicit true
#print foo

[Vincent Siles]

Thank you !