port to agda/2.5.4.1 and agda-stdlib/0.17
[~helmut/bidiragda.git] / Precond.agda
index 07775ac..98ba7a6 100644 (file)
@@ -11,13 +11,14 @@ open import Level using () renaming (zero to ℓ₀)
 import Category.Monad
 import Category.Functor
 open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
-open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
-open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
+import Data.Maybe.Categorical
+open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
+open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
 open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘)
 import Data.List.All
 open import Data.List.Any using (here ; there)
-open import Data.List.Any.Membership.Propositional using (_∉_)
+open import Data.List.Membership.Setoid using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
@@ -99,9 +100,9 @@ module _ (G : Get) where
 
 data All-different {A : Set} : List A → Set where
   different-[] : All-different []
-  different-∷  : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs)
+  different-∷  : {x : A} {xs : List A} → _∉_ (P.setoid A) x xs → All-different xs → All-different (x ∷ xs)
 
-lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing
+lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → _∉_ (P.setoid (Fin n)) i (toList is) → lookupM i h ≡ nothing
 lemma-∉-lookupM-assoc i []         []         P.refl i∉is = lemma-lookupM-empty i
 lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs')     ph i∉is with assoc is' xs' | inspect (assoc is') xs'
 lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs')     () i∉is | nothing | [ ph' ]