Mercurial > hg > Members > kono > Proof > automaton

diff agda/finiteSet.agda @ 87:217ef727574a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reverse direction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Nov 2019 17:15:18 +0900
parents 9911911b77cb
children e7b3a2856ccb
line wrap: on
line diff
--- a/agda/finiteSet.agda	Sat Nov 09 14:44:38 2019 +0900
+++ b/agda/finiteSet.agda	Sat Nov 09 17:15:18 2019 +0900
@@ -42,6 +42,10 @@
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
      ... | no ¬p = false
+     equal?-refl : {q : Q} → equal? q q ≡ true
+     equal?-refl {q} with F←Q q ≟ F←Q q
+     ... | yes p = refl
+     ... | no ne = ⊥-elim (ne refl)
      fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
      fin<n {_} {zero} = s≤s z≤n
      fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})