summaryrefslogtreecommitdiff
path: root/Instances.agda
diff options
context:
space:
mode:
authorHelmut Grohne <helmut@subdivi.de>2020-08-01 09:12:17 +0200
committerHelmut Grohne <helmut@subdivi.de>2020-08-01 09:12:17 +0200
commit1286deef698a9fbf92b86d0078fd62c47f980ee9 (patch)
treecf70314c5e62c774c225db342ec0c4bae3fd493d /Instances.agda
parent85865ec3c7c3e3a458dc233d4c28e4db97191f3d (diff)
downloadbidiragda-1286deef698a9fbf92b86d0078fd62c47f980ee9.tar.gz
move imports for agda-stdlib 1.3
Diffstat (limited to 'Instances.agda')
-rw-r--r--Instances.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/Instances.agda b/Instances.agda
index a09e30d..e59d8a1 100644
--- a/Instances.agda
+++ b/Instances.agda
@@ -7,7 +7,7 @@ import Data.Maybe.Categorical
open import Data.Nat using (ℕ)
open import Data.Product using (_×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Vec using (Vec)
-open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise-≡⇒≡)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-≡⇒≡)
open import Function using (_∘_ ; id)
open import Relation.Binary using (Setoid ; module Setoid)
open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSetoid to ISetoid)