# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1488288783 -32400
# Node ID 7ed0045e4adf63b01ff404e53c43e2ae8d1eae60
# Parent  3ee32e4df4c7a0bcf57e10e7beb57f0f46de7ccf
negnat

diff -r 3ee32e4df4c7 -r 7ed0045e4adf negnat.agda
--- a/negnat.agda	Tue Feb 28 12:38:23 2017 +0900
+++ b/negnat.agda	Tue Feb 28 22:33:03 2017 +0900
@@ -1,5 +1,3 @@
-
-
 module negnat where
 
 
@@ -21,6 +19,11 @@
 ℕ-elim P s z zero    = z
 ℕ-elim P s z (suc n) = s (ℕ-elim P s z n)
 
+-- data ⊥ : Set where
+
+-- record ⊤ : Set where
+--  constructor tt
+
 -- peano : ∀ n → suc n ≡ zero → ⊥
 
 Nope : (m n : ℕ) → Set
@@ -49,8 +52,9 @@
 Nope0 : ℕ → Set
 Nope0 = ℕ-elim (λ _ → Set) (λ _ → ⊤) ⊥
 
--- Nope1 zero    = ⊥
--- Nope1 (suc _) = ⊤
+Nope1  :  ℕ  -> Set 
+Nope1 zero    = ⊥
+Nope1 (suc _) = ⊤
 
 bad : Fin 0 → ⊥
 bad = Fin-elim (λ n _ → Nope0 n) (λ _ → _) _
@@ -68,10 +72,9 @@
 div (suc (suc n)) p = suc (div n p)
 div (suc zero) () 
 
-proof : (suc (suc zero) + (suc (suc (suc zero)))) ≡ (suc (suc (suc (suc (suc zero)))))
+proof : 2 + 3 ≡ suc (suc (suc (suc (suc zero)))) 
 proof = refl
 
--- data ⊥ : Set where
 --
 -- ¬_ : Set → Set
 -- ¬ A = A → ⊥