Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/finiteSetUtil.agda @ 383:708570e55a91

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add regex2 (we need source reorganization)
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Jul 2023 11:26:17 +0900
parents 21aa222b11c9
children c298981108c1
comparison
equal deleted inserted replaced
382:9fba498b0a7a 383:708570e55a91
131 open ≡-Reasoning 131 open ≡-Reasoning
132 132
133 data One : Set where 133 data One : Set where
134 one : One 134 one : One
135 135
136 finOne : FiniteSet One
137 finOne = record { finite = 1 ; Q←F = λ _ → one ; F←Q = λ _ → # 0 ; finiso→ = fin00 ; finiso← = fin1≡0 } where
138 fin00 : (q : One) → one ≡ q
139 fin00 one = refl
140
136 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 141 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B)
137 fin-∨1 {B} fb = record { 142 fin-∨1 {B} fb = record {
138 Q←F = Q←F 143 Q←F = Q←F
139 ; F←Q = F←Q 144 ; F←Q = F←Q
140 ; finiso→ = finiso→ 145 ; finiso→ = finiso→