update agda-stdlib

this leaves us at commit d1e0ae9c9c9c7c99900d1806fbdb4c5082fc76fc
dianne · Jan 20, 2019 · 7dc27a7 · 7dc27a7
1 parent 305ab60
commit 7dc27a7
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda
@@ -2,8 +2,8 @@ module Minesweeper.Board where
 
 open import Data.Vec as Vec using (Vec)
 import Data.Vec.Properties as VecProp
-import Data.Vec.Relation.Pointwise.Inductive   as VecIndPointwise
-import Data.Vec.Relation.Pointwise.Extensional as VecExtPointwise
+import Data.Vec.Relation.Binary.Pointwise.Inductive   as VecIndPointwise
+import Data.Vec.Relation.Binary.Pointwise.Extensional as VecExtPointwise
 open import Data.Fin using (_≟_)
 open import Data.Product
 open import Data.Product.Relation.Pointwise.NonDependent using (≡×≡⇒≡)

diff --git a/Minesweeper/Enumeration.agda b/Minesweeper/Enumeration.agda
@@ -3,7 +3,7 @@ module Minesweeper.Enumeration where
 open import Data.List as List using (List; []; _∷_)
 import Data.List.Categorical as List
 import Data.List.Properties as ListProp
-open import Data.List.Any as Any using (Any ; here ; there)
+open import Data.List.Relation.Unary.Any as Any using (Any ; here ; there)
 import Data.List.Any.Properties as AnyProp
 open import Data.List.Membership.Propositional
 import Data.List.Membership.Propositional.Properties as ∈Prop

diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda
@@ -6,9 +6,9 @@ open import Data.Empty
 open import Data.Product
 open import Data.Sum
 open import Data.Vec as Vec using (Vec; []; _∷_; _++_)
-open import Data.Vec.Relation.Pointwise.Inductive as VecPointwise using ([]; _∷_)
-open import Data.Vec.Any as Any using (Any; any)
-import      Data.Vec.Any.Properties as AnyProp
+open import Data.Vec.Relation.Unary.Any as Any using (Any; any)
+import      Data.Vec.Relation.Unary.Any.Properties as AnyProp
+open import Data.Vec.Relation.Binary.Pointwise.Inductive as VecPointwise using ([]; _∷_)
 open import Data.Vec.Membership.Propositional using (_∈_)
 import      Data.Vec.Membership.Propositional.Properties as ∈
 open import Data.Nat hiding (_>_; _≥_)

diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda
@@ -7,12 +7,12 @@ open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
 open import Data.Empty
 open import Data.List as List using (List; []; _∷_)
-open import Data.List.Relation.Pointwise as Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any.Properties using (there-injective)
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Membership.Propositional
-open import Data.List.All as All using (All; []; _∷_)
-open import Data.List.All.Properties using (All¬⇒¬Any)
-open import Data.List.Any as Any using (Any; here; there)
-open import Data.List.Any.Properties using (there-injective)
 open import Data.Product as Σ
 open import Data.Product.Properties
 open import Data.Nat