From 6ce567bf63a61bce4ccf71e3ec402d94d1da2fb1 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 29 Sep 2019 13:54:46 +0200
Subject: port to agda/2.6.0.1 and agda-stdlib/1.1

 * Data.Vec.lookup changed parameter order.
 * A number of symbols were moved from Data.Maybe to submodules.
 * In a number of occasions, agda no longer figures implicit arguments
   and they had to be made explicit.
 * We can no longer use heterogeneous proofs inside equational reasoning
   for propositional equality. Use heterogeneous equational reasoning.
 * Stop importing proof-irrelevance as that would require K.
---
 FinMap.agda | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'FinMap.agda')

diff --git a/FinMap.agda b/FinMap.agda
index 6342fc5..051014c 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -2,7 +2,8 @@ module FinMap where
 
 open import Level using () renaming (zero to ℓ₀)
 open import Data.Nat using (ℕ ; zero ; suc)
-open import Data.Maybe using (Maybe ; just ; nothing ; maybe′ ; just-injective)
+open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
+open import Data.Maybe.Properties using (just-injective)
 open import Data.Fin using (Fin ; zero ; suc)
 open import Data.Fin.Properties using (_≟_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
@@ -40,7 +41,7 @@ FinMapMaybe : ℕ → Set → Set
 FinMapMaybe n A = Vec (Maybe A) n
 
 lookupM : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → Maybe A
-lookupM = lookupVec
+lookupM = flip lookupVec
 
 insert : {A : Set} {n : ℕ} → Fin n → A → FinMapMaybe n A → FinMapMaybe n A
 insert f a m = m [ f ]≔ (just a)
@@ -129,6 +130,6 @@ lemma-disjoint-union {n} f t = tabulate-cong inner
             ≡⟨ P.cong (flip (maybe′ just) nothing) (lookup∘tabulate (just ∘ f) x) ⟩
           just (f x) ∎
 
-lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
-lemma-exchange-maps h≈h′ {[]}     All.[]         = P.refl
-lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)
+lemma-exchange-maps : {n m : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
+lemma-exchange-maps h h' h≈h′ {[]}     All.[]         = P.refl
+lemma-exchange-maps h h' h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h h' h≈h′ pis)
-- 
cgit v1.2.3