# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1399947289 -32400
# Node ID ca2e9f7a7898e09342069feab842faab21dea990
# Parent  f300bd2101d35b8a513ba4efb53f1543531a7ddf
Add De Morgan's laws

diff -r f300bd2101d3 -r ca2e9f7a7898 boolean.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/boolean.agda	Tue May 13 11:14:49 2014 +0900
@@ -0,0 +1,22 @@
+open import systemT
+open import Relation.Binary.PropositionalEquality
+
+module boolean where
+
+_and_ : Bool -> Bool -> Bool
+T and b = b
+F and _ = F
+
+_or_ : Bool -> Bool -> Bool
+T or _ = T
+F or b = b
+
+not : Bool -> Bool
+not T = F
+not F = T
+
+De-Morgan's-laws : (a b : Bool) -> (not a) and (not b) ≡ not (a or b)
+De-Morgan's-laws T T = refl
+De-Morgan's-laws T F = refl
+De-Morgan's-laws F T = refl
+De-Morgan's-laws F F = refl
diff -r f300bd2101d3 -r ca2e9f7a7898 systemT.agda
--- a/systemT.agda	Fri May 09 13:03:29 2014 +0900
+++ b/systemT.agda	Tue May 13 11:14:49 2014 +0900
@@ -15,3 +15,4 @@
 D : {U : Set} -> U -> U -> Bool -> U
 D u v F = v
 D u v T = u
+