diff automaton-in-agda/src/pumping.agda @ 403:c298981108c1

fix for std-lib 2.0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 11:32:01 +0900
parents 101080136450
children af8f630b7e60
line wrap: on
line diff
--- a/automaton-in-agda/src/pumping.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/pumping.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -65,7 +65,7 @@
 
 open Data.Maybe
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 open import Relation.Binary.Definitions
 open import Data.Unit using (⊤ ; tt)
 open import Data.Nat.Properties