diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-21 11:21:41 +0200 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-10-21 11:21:41 +0200 |
| commit | 6fa57da8105a0bad87c571ac911fa54d161745ad (patch) | |
| tree | 3f731ae8ddb10bfe801f048616c86d982d95e421 /Precond.agda | |
| parent | 2991f01c1867d6431d50d0e1309522b005de4bde (diff) | |
| download | bidiragda-6fa57da8105a0bad87c571ac911fa54d161745ad.tar.gz | |
move all those toList calls inside _in-domain-of_
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Precond.agda b/Precond.agda index 8d2eab2..31ac04b 100644 --- a/Precond.agda +++ b/Precond.agda @@ -40,7 +40,7 @@ lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.j lemma-maybe-just a (just x) = refl lemma-maybe-just a nothing = refl -lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → (toList is) in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v +lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∘ (λ f → begin maybe′ just (lookupM f (fromFunc g)) (lookupM f h) ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩ |