Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/automaton-ex.agda @ 405:af8f630b7e60

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 Sun, 24 Sep 2023 18:02:04 +0900
parents 407684f806e4
children
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2
2 module automaton-ex where 3 module automaton-ex where
3 4
4 open import Data.Nat 5 open import Data.Nat
5 open import Data.List 6 open import Data.List
6 open import Data.Maybe 7 open import Data.Maybe
100 ... | no n = count-chars t x 101 ... | no n = count-chars t x
101 102
102 test11 : count-chars ( i1 ∷ i1 ∷ i0 ∷ [] ) i0 ≡ 1 103 test11 : count-chars ( i1 ∷ i1 ∷ i0 ∷ [] ) i0 ≡ 1
103 test11 = refl 104 test11 = refl
104 105
106 _≥b_ : ( x y : ℕ) → Bool
107 x ≥b y with <-cmp x y
108 ... | tri< a ¬b ¬c = false
109 ... | tri≈ ¬a b ¬c = true
110 ... | tri> ¬a ¬b c = true
111
112 _>b_ : ( x y : ℕ) → Bool
113 x >b y with <-cmp x y
114 ... | tri< a ¬b ¬c = false
115 ... | tri≈ ¬a b ¬c = false
116 ... | tri> ¬a ¬b c = true
117
118 _≤b_ : ( x y : ℕ) → Bool
119 x ≤b y = y ≥b x
120
121 _<b_ : ( x y : ℕ) → Bool
122 x <b y = y >b x
123
105 ex1_4a : (x : List In2) → Bool 124 ex1_4a : (x : List In2) → Bool
106 ex1_4a x = ( count-chars x i0 ≥b 3 ) /\ ( count-chars x i1 ≥b 2 ) 125 ex1_4a x = ( count-chars x i0 ≥b 3 ) /\ ( count-chars x i1 ≥b 2 )
107 126
108 language' : { Σ : Set } → Set 127 language' : { Σ : Set } → Set
109 language' {Σ} = List Σ → Bool 128 language' {Σ} = List Σ → Bool
136 155
137 am14a-tr' : am14s → In2 → am14s 156 am14a-tr' : am14s → In2 → am14s
138 am14a-tr' a00 i0 = a10 157 am14a-tr' a00 i0 = a10
139 am14a-tr' _ _ = a10 158 am14a-tr' _ _ = a10
140 159
141 am14a' : Automaton am14s In2 160 -- am14a' : Automaton am14s In2
142 am14a' = record { δ = am14a-tr' ; aend = λ x → {!!} } 161 -- am14a' = record { δ = am14a-tr' ; aend = λ x → {!!} }