Mercurial > hg > Members > kono > Proof > automaton

diff 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
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 24 19:01:09 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 25 11:26:17 2023 +0900
@@ -133,6 +133,11 @@
 data One : Set where
    one : One
 
+finOne : FiniteSet One
+finOne =  record { finite = 1 ;  Q←F = λ _ → one ; F←Q = λ _ → # 0 ; finiso→ = fin00 ; finiso← = fin1≡0  }  where
+    fin00 : (q : One) → one ≡ q
+    fin00 one = refl
+
 fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) 
 fin-∨1 {B} fb =  record {
        Q←F = Q←F