Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/regular-language.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 62a4d1a2c48d
children a60132983557
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 module regular-language where 3 module regular-language where
2 4
3 open import Level renaming ( suc to Suc ; zero to Zero ) 5 open import Level renaming ( suc to Suc ; zero to Zero )
4 open import Data.List 6 open import Data.List
5 open import Data.Nat hiding ( _≟_ ) 7 open import Data.Nat hiding ( _≟_ )
29 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t 31 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
30 32
31 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} 33 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
32 Concat {Σ} A B = split A B 34 Concat {Σ} A B = split A B
33 35
34 {-# TERMINATING #-} 36 -- {-# TERMINATING #-}
35 Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ} 37 -- Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
36 Star1 {Σ} A [] = true 38 -- Star1 {Σ} A [] = true
37 Star1 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t) 39 -- Star0 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t)
38 40
39 -- Terminating version of Star1 41 -- Terminating version of Star1
40 -- 42 --
41 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 43 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool
42 repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool 44 repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool