Search code examples
singletoncoqtypeclass

Singleton Classes in Coq

I don't really understand singleton classes in Coq. I am currently looking at the following definition:

Class Decision (P : Prop) := decide : {P} + {¬P}.

As far as I undestand this creates the singleton class Decision P and a function decide: forall (P: Prop), Decision P -> {P} + {¬P}.

But how do I create inhabitants of Decision P which I seem to need to use decide? There does not seem to be any constructor.

Solution

  • As stated in the comments, from my understanding Class is used to define a typeclass.

    Following this link, if you want to make something a member of your type class Decision you have to define an instance as well: 

    instance DecidableT : Decision T {
    decide := ...
}.