Mercurial > hg > Members > atton > agda > systemT

changeset 2:ca2e9f7a7898

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add De Morgan's laws
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 13 May 2014 11:14:49 +0900
parents f300bd2101d3
children 7138e79615b3
files boolean.agda systemT.agda
diffstat 2 files changed, 23 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /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
--- 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
+