How to prove decidability for Nonempty

Stream: new members

[Eric Wieser]

jsodd said:

Another question about decidability: why Nonempty \R also runs into decidability issues? It seems to have nothing to do with computations...

Can you ask that question with a #mwe ?

[jsodd]

Eric Wieser said:

Can you ask that question with a #mwe ?

import Mathlib.Data.Real.Basic

#eval Nonempty ℝ

[Eric Wieser]

This works:

set_option checkBinderAnnotations false in
/-- Anything that typeclass search can find is decidable -/
instance decidableTypeClassOfInstance {P} [P] : Decidable P := .isTrue ‹_›

[Eric Wieser]

@Kyle Miller or @Matthew Ballard probably can tell you why that instance is a terrible idea

[Eric Wieser]

Alternatively, perhaps #eval should raise an error if you pass it a typeclass, and should say "use synth instead"

[Kyle Miller]

It wouldn't hurt adding Decidable instances for some of these property classes, one at a time rather than than Eric's blanket instance (I don't know what happens if P is not a class).

import Mathlib.Data.Real.Basic

instance {α : Sort*} [Nonempty α] : Decidable (Nonempty α) := isTrue inferInstance

#eval Nonempty ℝ
-- true