diff options
| author | Arthur Azevedo de Amorim | 2019-10-25 03:47:31 -0400 |
|---|---|---|
| committer | Assia Mahboubi | 2019-10-25 09:47:31 +0200 |
| commit | efa0b18767f3310507088749b203e5c0b5e96d5a (patch) | |
| tree | 826efea4bae1ea44918bb31ab57506212928febf /mathcomp/ssreflect/eqtype.v | |
| parent | 6542e973cdc5d10dce2e7b7b7230a804dda4e73b (diff) | |
Instances for empty type. (#393)
* Add notation and instances for empty type.
* Update change log.
* Mention void in fintype header.
* Remove unnecessary explicit argument.
* Documentation header for void.
Diffstat (limited to 'mathcomp/ssreflect/eqtype.v')
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 7e1cdc8..e9da3ec 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -765,6 +765,9 @@ Arguments val_eqP {T P sT x y}. Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T) (at level 0, format "[ 'eqMixin' 'of' T 'by' <: ]") : form_scope. +Definition void_eqMixin := PcanEqMixin (of_voidK unit). +Canonical void_eqType := EqType void void_eqMixin. + Section SigEqType. Variables (T : eqType) (P : pred T). |