diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/FinMap.agda b/FinMap.agda index a85f119..1fc2d16 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -64,18 +64,10 @@ partialize = mapV just lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever lemma-just≢nothing refl () -module Private {S : Setoid ℓ₀ ℓ₀} where - private - open Setoid S - reflMaybe = Setoid.refl (MaybeEq S) - _≈Maybe_ = Setoid._≈_ (MaybeEq S) - - lemma-insert-same : {n : ℕ} → (m : FinMapMaybe n Carrier) → (f : Fin n) → (a : Carrier) → lookupM f m ≈Maybe just a → Setoid._≈_ (vecIsSetoid (MaybeEq S) n) m (insert f a m) - lemma-insert-same [] () a p - lemma-insert-same {suc n} (x ∷ xs) zero a p = p ∷-cong Setoid.refl (vecIsSetoid (MaybeEq S) n) - lemma-insert-same (x ∷ xs) (suc i) a p = reflMaybe ∷-cong lemma-insert-same xs i a p - -open Private public +lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → (a : A) → lookupM f m ≡ just a → m ≡ insert f a m +lemma-insert-same [] () a p +lemma-insert-same {suc n} (x ∷ xs) zero a p = cong (flip _∷_ xs) p +lemma-insert-same (x ∷ xs) (suc i) a p = cong (_∷_ x) (lemma-insert-same xs i a p) lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing lemma-lookupM-empty zero = refl |