Mercurial > hg > Members > kono > Proof > automaton

diff automaton-in-agda/src/finiteSet.agda @ 318:91781b7c65a8

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 Thu, 06 Jan 2022 07:27:52 +0900
parents d1e8e5eadc38
children c298981108c1
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSet.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/finiteSet.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -3,7 +3,7 @@
 
 open import Data.Nat hiding ( _≟_ )
 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
--- open import Data.Fin.Properties
+-- open import Data.Fin.Properties  hiding ( ≤-refl )
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary.Definitions