## Stream: lean4

### Topic: decidable equality instances

#### Jason Gross (Mar 22 2021 at 18:58):

Why does deriving instance BEq for ... not result in decide (_ = _) succeeding? Also, why is there not already an instance for decidable equality of Lean.MessageSeverity?

#### Jason Gross (Mar 22 2021 at 18:59):

Ah, I guess I want deriving instance DecidableEq for Lean.MessageSeverity same question, though, about it not already existing

#### Sebastian Ullrich (Mar 22 2021 at 19:06):

I suppose we only used match to handle it so far

#### Jason Gross (Mar 22 2021 at 19:08):

Is it worth making a PR adding deriving? (Or adding such deriving to all the data in Lean and the stdlib more systematically?)

Last updated: May 18 2021 at 23:14 UTC