Merge branch feature-delete
[~helmut/bidiragda.git] / Precond.agda
index 6aba291..19329b5 100644 (file)
@@ -20,18 +20,18 @@ open Data.List.Any.Membership-≡ using (_∉_)
 open import Data.Maybe using (just)
 open import Data.Product using (∃ ; _,_ ; proj₂)
 open import Function using (flip ; _∘_ ; id)
-open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
+open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
 open import Generic using (mapMV ; sequenceV ; sequence-map)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete)
 import CheckInsert
-open CheckInsert Carrier deq using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
+open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
 import BFF
-open import Bidir Carrier deq using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
+open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
 
-open BFF.VecBFF Carrier deq using (get-type ; assoc ; enumerate ; denumerate ; bff)
+open BFF.VecBFF (decSetoid deq) using (get-type ; assoc ; enumerate ; denumerate ; bff)
 
 lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v)
 lemma-lookup-map-just zero    (x ∷ xs) = refl