diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-05 15:59:06 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-05 15:59:06 +0100 |
| commit | 95609983219f14e8f4c0758cd0688b984d8b1455 (patch) | |
| tree | 497e596edcbca0a745d1a42fb1995dc731631dac /Precond.agda | |
| parent | 5f11a53df7da1df3757cf8fd54652f78a50afbf0 (diff) | |
| download | bidiragda-95609983219f14e8f4c0758cd0688b984d8b1455.tar.gz | |
be more precise about which lookups we use
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 10 |
1 files changed, 5 insertions, 5 deletions
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))) ∎) |