diff options
| -rw-r--r-- | BFF.agda | 2 | ||||
| -rw-r--r-- | Bidir.agda | 4 | ||||
| -rw-r--r-- | Precond.agda | 10 |
3 files changed, 8 insertions, 8 deletions
@@ -40,4 +40,4 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where g′ = delete-many t′ g h = assoc t′ v h′ = (flip union g′) <$> h - in h′ >>= flip mapMV s′ ∘ flip lookupV + in h′ >>= flip mapMV s′ ∘ flip lookupM @@ -141,7 +141,7 @@ theorem-1 G s = begin ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩ (h′↦r ∘ just) (fromFunc (denumerate s)) ≡⟨ refl ⟩ - mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s) + mapMV (flip lookupM (fromFunc (denumerate s))) (enumerate s) ≡⟨ mapMV-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s) ⟩ mapMV (Maybe.just ∘ denumerate s) (enumerate s) ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩ @@ -151,7 +151,7 @@ theorem-1 G s = begin where open ≡-Reasoning open Get G h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) - h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) + h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupM) lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a diff --git a/Precond.agda b/Precond.agda index 312fbde..354e5f1 100644 --- a/Precond.agda +++ b/Precond.agda @@ -43,11 +43,11 @@ lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : Fi lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin union h (fromFunc g) ≡⟨ lemma-tabulate-∘ (λ f → begin - maybe′ just (lookup f (fromFunc g)) (lookup f h) - ≡⟨ cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-fromFunc g f) ⟩ - maybe′ just (just (g f)) (lookup f h) - ≡⟨ lemma-maybe-just (g f) (lookup f h) ⟩ - just (maybe′ id (g f) (lookup f h)) ∎) ⟩ + maybe′ just (lookupM f (fromFunc g)) (lookupM f h) + ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩ + maybe′ just (just (g f)) (lookupM f h) + ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩ + just (maybe′ id (g f) (lookupM f h)) ∎) ⟩ tabulate (λ f → just (maybe′ id (g f) (lookup f h))) ≡⟨ tabulate-∘ just (λ f → maybe′ id (g f) (lookup f h)) ⟩ map just (tabulate (λ f → maybe′ id (g f) (lookup f h))) ∎) |