Mercurial > hg > Members > kono > Proof > automaton

diff agda/regex1.agda @ 41:ae69102153a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cfg done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Dec 2018 01:30:03 +0900
parents 3f099f353f1c
children aa15eff1aeb3
line wrap: on
line diff
--- a/agda/regex1.agda	Fri Dec 21 23:06:32 2018 +0900
+++ b/agda/regex1.agda	Sat Dec 22 01:30:03 2018 +0900
@@ -40,7 +40,7 @@
       → ( List Σ → Bool) → List Σ → Bool
 split x y  [] = x [] ∧ y []
 split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
-  split (λ t1 → x ( ( h ∷ [] ) ++ t1 ))  (λ t2 → y t2 ) t
+  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
 {-# TERMINATING #-}
 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool