Mercurial > hg > Members > kono > Proof > category

changeset 452:7ed0045e4adf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
negnat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Feb 2017 22:33:03 +0900
parents 3ee32e4df4c7
children 3c2ce4474d92
files negnat.agda
diffstat 1 files changed, 9 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- 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 → ⊥