Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/pumping.agda @ 403:c298981108c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for std-lib 2.0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 11:32:01 +0900
parents 101080136450
children af8f630b7e60
comparison
equal deleted inserted replaced
402:093e386c10a2 403:c298981108c1
63 tr→qs=is fa .[] q (tend x) = refl 63 tr→qs=is fa .[] q (tend x) = refl
64 tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is (δ fa q i) tr) 64 tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is (δ fa q i) tr)
65 65
66 open Data.Maybe 66 open Data.Maybe
67 67
68 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 68 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
69 open import Relation.Binary.Definitions 69 open import Relation.Binary.Definitions
70 open import Data.Unit using (⊤ ; tt) 70 open import Data.Unit using (⊤ ; tt)
71 open import Data.Nat.Properties 71 open import Data.Nat.Properties
72 72
73 data QDSEQ { Q : Set } { Σ : Set } { fa : Automaton Q Σ} ( finq : FiniteSet Q) (qd : Q) (z1 : List Σ) : 73 data QDSEQ { Q : Set } { Σ : Set } { fa : Automaton Q Σ} ( finq : FiniteSet Q) (qd : Q) (z1 : List Σ) :