diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-04 10:52:49 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-04 10:52:49 +0100 |
| commit | 20c176d383e59a0345f7425c5f14679906159a59 (patch) | |
| tree | a2874cac4922670c6d8e8229c24b56a725c11dda /Precond.agda | |
| parent | 257665f2910296c6e87113d2f7a418e1f83b33f6 (diff) | |
| download | bidiragda-20c176d383e59a0345f7425c5f14679906159a59.tar.gz | |
add convenience members to PartialVecVec.Get
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 787f010..81c204b 100644 --- a/Precond.agda +++ b/Precond.agda @@ -74,7 +74,7 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Da maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎ inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i) -assoc-enough : (G : Get) → {i : Setoid.Carrier (Get.I G)} → (s : Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)) → (v : Vec Carrier (Get.gl₂ G ⟨$⟩ i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u +assoc-enough : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u assoc-enough G s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin bff G s v ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩ |