# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572411817 -32400
# Node ID 475923938f503bed4a4df272a3c72035c3b38c63
# Parent  abfeed0c61b5e4509850bbeb78cea6afb0fbfe1b
...

diff -r abfeed0c61b5 -r 475923938f50 agda/automaton.agda
--- a/agda/automaton.agda	Wed Oct 30 12:07:29 2019 +0900
+++ b/agda/automaton.agda	Wed Oct 30 14:03:37 2019 +0900
@@ -8,6 +8,7 @@
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import logic
+-- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )
 
 record Automaton ( Q : Set ) ( Σ : Set  )
        : Set  where
diff -r abfeed0c61b5 -r 475923938f50 agda/logic.agda
--- a/agda/logic.agda	Wed Oct 30 12:07:29 2019 +0900
+++ b/agda/logic.agda	Wed Oct 30 14:03:37 2019 +0900
@@ -7,8 +7,8 @@
 
 
 data Bool : Set where
-   true : Bool
-   false : Bool
+    true : Bool
+    false : Bool
 
 record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
    field
@@ -48,3 +48,17 @@
 infixr  140 _∨_
 infixr  150 _⇔_
 
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+infixr  130 _\/_
+infixr  140 _/\_