diff options
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Precond.agda b/Precond.agda index 6aba291..19329b5 100644 --- a/Precond.agda +++ b/Precond.agda @@ -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 |