Mercurial > hg > Members > kono > Proof > automaton

diff automaton-in-agda/src/finiteSetUtil.agda @ 406:a60132983557

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 08 Nov 2023 21:35:54 +0900
parents af8f630b7e60
children
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -371,6 +371,10 @@
 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n)
 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
 
+--
+-- fin→ is in finiteFunc.agda
+--      we excludeit becauase it uses f-extensionarity
+
 open import Data.List
 
 open FiniteSet