Mercurial > hg > Members > kono > Proof > automaton

diff automaton-in-agda/src/finiteSet.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 c298981108c1
children
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSet.agda	Wed Nov 29 17:40:55 2023 +0900
+++ b/automaton-in-agda/src/finiteSet.agda	Fri Apr 05 13:38:20 2024 +0900
@@ -40,3 +40,12 @@
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
      ... | no ¬p = false
+
+record FiniteSetF ( Q : Set ) : Set  where
+     field
+        finite : ℕ
+        Q←F : Fin finite → Q → Bool
+        F←Q : (Q → Bool) → Fin finite
+        finiso→ : (f : Q → Bool ) → (q : Q) → Q←F ( F←Q f ) q ≡ f q
+        finiso← : (f : Fin finite ) → F←Q ( Q←F f )  ≡ f 
+