From 9607518ce04bee569f781e069e7e5dcda3e0f6f6 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Tue, 16 Dec 2014 14:22:54 -0500
Subject: [PATCH] chore(hott) reflect @avigad's name changes in the std library

---
 hott/init/logic.hlean       | 12 ++++++------
 hott/init/types/empty.hlean | 20 --------------------
 hott/logic.hlean            |  3 ++-
 3 files changed, 8 insertions(+), 27 deletions(-)

diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 63ec2712a..a4b12c57f 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -19,20 +19,20 @@ assume Ha : a, absurd (H₁ Ha) H₂
 -- not
 -- ---
 
-definition not_empty : ¬ empty :=
+protected definition not_empty : ¬ empty :=
 assume H : empty, H
 
 definition not_not_intro {a : Type} (Ha : a) : ¬¬a :=
 assume Hna : ¬a, absurd Ha Hna
 
-definition not_intro {a : Type} (H : a → empty) : ¬a := H
+definition not.intro {a : Type} (H : a → empty) : ¬a := H
 
-definition not_elim {a : Type} (H₁ : ¬a) (H₂ : a) : empty := H₁ H₂
+definition not.elim {a : Type} (H₁ : ¬a) (H₂ : a) : empty := H₁ H₂
 
-definition not_implies_left {a b : Type} (H : ¬(a → b)) : ¬¬a :=
+definition not_not_of_not_implies {a b : Type} (H : ¬(a → b)) : ¬¬a :=
 assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H
 
-definition not_implies_right {a b : Type} (H : ¬(a → b)) : ¬b :=
+definition not_of_not_implies {a b : Type} (H : ¬(a → b)) : ¬b :=
 assume Hb : b, absurd (assume Ha : a, Hb) H
 
 -- eq
@@ -43,7 +43,7 @@ definition rfl {A : Type} {a : A} := eq.refl a
 
 namespace eq
   variables {A : Type}
-  variables {a b c a': A}
+  variables {a b c a' : A}
 
   definition subst {P : A → Type} (H₁ : a = b) (H₂ : P a) : P b :=
   rec H₂ H₁
diff --git a/hott/init/types/empty.hlean b/hott/init/types/empty.hlean
index 383e234b8..ef96e6362 100644
--- a/hott/init/types/empty.hlean
+++ b/hott/init/types/empty.hlean
@@ -14,23 +14,3 @@ end empty
 
 protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
 take (a b : empty), decidable.inl (!empty.elim a)
-
-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
diff --git a/hott/logic.hlean b/hott/logic.hlean
index 2660e3e7c..a422a9e5b 100644
--- a/hott/logic.hlean
+++ b/hott/logic.hlean
@@ -1,9 +1,10 @@
 --javra:        Maybe this should go somewhere else
 
 open eq
+
 inductive tdecidable [class] (A : Type) : Type :=
 inl :  A → tdecidable A,
-inr : ~A → tdecidable A
+inr : ¬A → tdecidable A
 
 structure decidable_paths [class] (A : Type) :=
 (elim : ∀(x y : A), tdecidable (x = y))