Zulip Chat Archive

Stream: lean4

Topic: decidable equality instances


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Mar 22 2021 at 19:06):

I suppose we only used match to handle it so far

view this post on Zulip 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