Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/cfg1.agda @ 412:b85402051cdb default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add mul
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Apr 2024 13:38:20 +0900
parents af8f630b7e60
children
comparison
equal deleted inserted replaced
411:207e6c4e155c 412:b85402051cdb
57 → ( List Σ → Bool) → List Σ → Bool 57 → ( List Σ → Bool) → List Σ → Bool
58 split x y [] = x [] /\ y [] 58 split x y [] = x [] /\ y []
59 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/ 59 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
60 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t 60 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
61 61
62
63 --
64 -- we can rewrite cfg-language without Termination check violation
65 --
62 66
63 cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool 67 cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool
64 68
65 {-# TERMINATING #-} 69 {-# TERMINATING #-}
66 cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool 70 cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool