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 623c99f..34c24fd 100644 --- a/Precond.agda +++ b/Precond.agda @@ -1,4 +1,4 @@ -open import Relation.Binary.Core using (Decidable) +open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality using (_≡_) module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where @@ -16,8 +16,8 @@ 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-∘ ; lookup-replicate ; tabulate-cong ; lookup∘tabulate ; lookup∘update′) -import Data.List.All -open import Data.List.Any using (here ; there) +import Data.List.Relation.Unary.All +open import Data.List.Relation.Unary.Any using (here ; there) open import Data.List.Membership.Setoid using (_∉_) open import Data.Maybe using (just) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) @@ -49,7 +49,7 @@ lemma-union-delete-fromFunc {is = []} h {g = g} p = _ , (tabulate-cong (λ f → ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩ just (maybe′ id (g f) (lookupM f h)) ∎)) where open ≡-Reasoning -lemma-union-delete-fromFunc {n = n} {is = i ∷ is} h {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin +lemma-union-delete-fromFunc {n = n} {is = i ∷ is} h {g = g} (Data.List.Relation.Unary.All._∷_ (x , px) ps) = _ , (begin union h (delete i (delete-many is (fromFunc g))) ≡⟨ tabulate-cong inner ⟩ union h (delete-many is (fromFunc g)) |