From 780e9499929d0e076af3c56c30a2c1a757015583 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Sat, 8 Nov 2014 20:55:42 -0500
Subject: [PATCH] feat(empty): define negation of types

---
 library/data/empty.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/library/data/empty.lean b/library/data/empty.lean
index 817ace12a..e1fbcd9ad 100644
--- a/library/data/empty.lean
+++ b/library/data/empty.lean
@@ -16,3 +16,23 @@ namespace empty
   protected theorem subsingleton [instance] : subsingleton empty :=
   subsingleton.intro (λ a b, !elim a)
 end empty
+
+definition tneg.tneg (A : Type) := A → empty
+prefix `~` := tneg.tneg
+namespace tneg
+variables {A B : Type}
+protected definition intro (H : A → empty)        : ~A     := H
+protected definition elim  (H1 : ~A) (H2 : A)     : empty  := H1 H2
+protected definition empty                        : ~empty := λH : empty, H
+definition tabsurd         (H1 : A) (H2 : ~A)     : B      := !empty.elim (H2 H1)
+definition tneg_tneg_intro (H : A)                : ~~A    := λH2 : ~A, tneg.elim H2 H
+definition tmt             (H1 : A → B) (H2 : ~B) : ~A     := λHA : A, tabsurd (H1 HA) H2
+
+definition tneg_pi_left {B : A → Type} (H : ~Πa, B a) : ~~A :=
+λHnA : ~A, tneg.elim H (λHA : A, tabsurd HA HnA)
+
+definition tneg_function_right (H : ~(A → B)) : ~B :=
+λHB : B, tneg.elim H (λHA : A, HB)
+
+
+end tneg