Mercurial > hg > Members > kono > Proof > automaton

diff agda/finiteSet.agda @ 70:702ce92c45ab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add concat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 06 Nov 2019 23:19:53 +0900
parents f124fceba460
children 7b357b295272
line wrap: on
line diff
--- a/agda/finiteSet.agda	Wed Nov 06 17:18:58 2019 +0900
+++ b/agda/finiteSet.agda	Wed Nov 06 23:19:53 2019 +0900
@@ -15,6 +15,8 @@
         F←Q : Q → Fin n
         finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
         finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+     finℕ : ℕ
+     finℕ = n
      lt0 : (n : ℕ) →  n Data.Nat.≤ n
      lt0 zero = z≤n
      lt0 (suc n) = s≤s (lt0 n)