Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello,

I have a use case. In one of my developments I represent directed graphs as 

{vertex : finType ; edge : finType ; source, target : edge -> vertex ; ... }

There I need the empty type as finType for graphs without edges. Below are my 
instances. 

So yes, I second including this in future releases.

Best,
Christian


-------------------------------------------------------------------

Inductive void : Type :=.

Lemma void_eqP : @Equality.axiom void [rel _ _ | false].
Proof. by case. Qed.

Canonical void_eqType := EqType void (EqMixin void_eqP).

Lemma void_pcancel : pcancel (fun x : void => match x with end) (fun x:unit 
=> None).
Proof. by case. Qed.

Definition void_choiceMixin := PcanChoiceMixin void_pcancel.
Canonical void_choiceType := ChoiceType void void_choiceMixin.
Definition void_countMixin := PcanCountMixin void_pcancel.
Canonical void_countType := CountType void void_countMixin.

Lemma void_enumP : @Finite.axiom [countType of void] [::].
Proof. by case. Qed.

Canonical void_finType := FinType void (FinMixin void_enumP).

--------------------------------------------------------------------





On 10/12/2017 08:38 AM, Maxime Dénès wrote:
> Hi Arthur,
> 
> That's an interesting observation. Just curious, what use cases do you
> have in mind?
> 
> Maxime.
> 
> On 10/12/2017 12:11 AM, Arthur Azevedo de Amorim wrote:
>> I was hoping to find instances of the basic ssreflect classes for
>> Empty_set or some other empty type, and to my surprise there aren't
>> any.  (The eqtype library still says: "The eqType interface is
>> implemented for most standard datatypes: bool, unit, void, ...".)
>>
>> Do others think it would be useful to include that in a future release?
>>
>> Arthur