diff options
| author | Théo Zimmermann | 2019-10-23 16:04:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-10-23 16:04:32 +0200 |
| commit | e6991dce306c41352c359a8ba5d6d9d6c5e6dfb2 (patch) | |
| tree | 4a64867766bc6978612516f3198a0348dc714440 | |
| parent | 0a2130e19c7f9af31e0a2eee74bf24af9619d0ec (diff) | |
| parent | b70084255c48479c061e7c0407359ceadc48e72f (diff) | |
Merge PR #10932: Add a notation for the empty type.
Reviewed-by: Zimmi48
Reviewed-by: amahboubi
| -rw-r--r-- | doc/changelog/06-ssreflect/10932-void-type-ssr.rst | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 13 |
2 files changed, 16 insertions, 0 deletions
diff --git a/doc/changelog/06-ssreflect/10932-void-type-ssr.rst b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst new file mode 100644 index 0000000000..7366ef1190 --- /dev/null +++ b/doc/changelog/06-ssreflect/10932-void-type-ssr.rst @@ -0,0 +1,3 @@ +- Add a :g:`void` notation for the standard library empty type (:g:`Empty_set`) + (`#10932 <https://github.com/coq/coq/pull/10932>`_, by Arthur Azevedo de + Amorim). 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. |