diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2018-11-25 11:29:53 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2018-11-25 11:29:53 +0100 |
| commit | 25d4df9182c92ef26979566f06c7c9f17746f0fb (patch) | |
| tree | 9fb198f637098799730a4f2fd1f30afcfe8182e1 /Precond.agda | |
| parent | 7fcd0fde85d545abbdae2265e173650c12d9b4c2 (diff) | |
| download | bidiragda-25d4df9182c92ef26979566f06c7c9f17746f0fb.tar.gz | |
port to agda/2.5.4.1 and agda-stdlib/0.17
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/Precond.agda b/Precond.agda index 07775ac..98ba7a6 100644 --- a/Precond.agda +++ b/Precond.agda @@ -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' ] |