Definition of Decidable

Stream: lean4

[Wrenna Robson]

Am I correct in saying that there was some talk of changing the definition of Decidable at some point, possibly to DecidablePred r being a function f : α -> Bool and a proof that f a = true \iff r a? I can't find the conversation in question. I'm not proposing making the change (or not making it!) - this kind of thing is "above my paygrade" really - but I was interested in what the current thinking was.

[Henrik Böving]

See https://github.com/leanprover/lean4/pull/2038 and the related discussions that emerged from it.

[Wrenna Robson]

Aha - it's probable I am remembering reading some discussion about lean4#8309, which seems to be still in progress (but I imagine not exactly a quick merge...).

[Wrenna Robson]

Thank you for the very quick reply!