Mercurial > hg > Members > Moririn

comparison logic.agda @ 586:0ddfa505d612

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isolate search function problem, and add hoareBinaryTree.agda.
author ryokka
date Wed, 04 Dec 2019 15:42:47 +0900
parents 821d04c0770b
children 2075785a124a
comparison
equal deleted inserted replaced
585:42e8cf963c5c 586:0ddfa505d612
1 module logic where 1 module logic where
2 2
3 open import Level 3 open import Level
4 open import Relation.Nullary 4 open import Relation.Nullary
5 open import Relation.Binary 5 open import Relation.Binary
6 open import Relation.Binary.PropositionalEquality
7
6 open import Data.Empty 8 open import Data.Empty
9 open import Data.Nat hiding (_⊔_)
7 10
8 11
9 data Bool : Set where 12 data Bool : Set where
10 true : Bool 13 true : Bool
11 false : Bool 14 false : Bool
50 53
51 _/\_ : Bool → Bool → Bool 54 _/\_ : Bool → Bool → Bool
52 true /\ true = true 55 true /\ true = true
53 _ /\ _ = false 56 _ /\ _ = false
54 57
58 _<B?_ : ℕ → ℕ → Bool
59 ℕ.zero <B? x = true
60 ℕ.suc x <B? ℕ.zero = false
61 ℕ.suc x <B? ℕ.suc xx = x <B? xx
62
63 -- _<BT_ : ℕ → ℕ → Set
64 -- ℕ.zero <BT ℕ.zero = ⊤
65 -- ℕ.zero <BT ℕ.suc b = ⊤
66 -- ℕ.suc a <BT ℕ.zero = ⊥
67 -- ℕ.suc a <BT ℕ.suc b = a <BT b
68
69
70 _≟B_ : Decidable {A = Bool} _≡_
71 true ≟B true = yes refl
72 false ≟B false = yes refl
73 true ≟B false = no λ()
74 false ≟B true = no λ()
75
55 _\/_ : Bool → Bool → Bool 76 _\/_ : Bool → Bool → Bool
56 false \/ false = false 77 false \/ false = false
57 _ \/ _ = true 78 _ \/ _ = true
58 79
59 not_ : Bool → Bool 80 not_ : Bool → Bool