Mercurial > hg > Members > kono > Proof > automaton

changeset 64:475923938f50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 30 Oct 2019 14:03:37 +0900
parents abfeed0c61b5
children 293a2075514b
files agda/automaton.agda agda/logic.agda
diffstat 2 files changed, 17 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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
--- 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 _/\_