decidable equality instances

Stream: lean4

[Jason Gross]

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]

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

[Sebastian Ullrich]

I suppose we only used match to handle it so far

[Jason Gross]

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