From fc0c2e19e763a4d3b4cbdb490950e0f85558e5c9 Mon Sep 17 00:00:00 2001
From: Arthur Azevedo de Amorim
Date: Tue, 22 Oct 2019 09:47:01 -0400
Subject: Add a notation for the empty type.

---
 plugins/ssr/ssrfun.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index dc774e811e..b8affba541 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -56,6 +56,10 @@ Require Import ssreflect.
                     Structure inference, as in the implementation of
                     the mxdirect predicate in matrix.v.
 
+ - The empty type:
+            void == a notation for the Empty_set type of the standard library.
+       of_void T == the canonical injection void -> T.
+
  - Sigma types:
            tag w == the i of w : {i : I & T i}.
         tagged w == the T i component of w : {i : I & T i}.
@@ -483,6 +487,12 @@ Arguments idfun {T} x /.
 
 Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2.
 
+(** The empty type. **)
+
+Notation void := Empty_set.
+
+Definition of_void T (x : void) : T := match x with end.
+
 (**  Strong sigma types.  **)
 
 Section Tag.
@@ -642,6 +652,9 @@ End Injections.
 Lemma Some_inj {T : nonPropType} : injective (@Some T).
 Proof. by move=> x y []. Qed.
 
+Lemma of_voidK T : pcancel (of_void T) [fun _ => None].
+Proof. by case. Qed.
+
 (**  cancellation lemmas for dependent type casts. **)
 Lemma esymK T x y : cancel (@esym T x y) (@esym T y x).
 Proof. by case: y /. Qed.
-- 
cgit v1.2.3