From 1428e4192d61533864a8f163c86272eef4b891cf Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 27 Sep 2012 13:11:53 +0200 Subject: move definition of get-type to BFF and use it everywhere --- Precond.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Precond.agda') diff --git a/Precond.agda b/Precond.agda index ba8c203..18d6a85 100644 --- a/Precond.agda +++ b/Precond.agda @@ -17,9 +17,9 @@ open import CheckInsert using (EqInst ; checkInsert ; lemma-checkInsert-new) open import BFF using (fmap ; _>>=_) open import Bidir using (lemma-∉-lookupM-assoc) -open BFF.VecBFF using (assoc ; enumerate ; denumerate ; bff) +open BFF.VecBFF using (get-type ; assoc ; enumerate ; denumerate ; bff) -assoc-enough : {getlen : ℕ → ℕ} (get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)) → {B : Set} {m : ℕ} → (eq : EqInst B) → (s : Vec B m) → (v : Vec B (getlen m)) → (h : FinMapMaybe m B) → assoc eq (get (enumerate s)) v ≡ just h → ∃ λ u → bff get eq s v ≡ just u +assoc-enough : {getlen : ℕ → ℕ} (get : get-type getlen) → {B : Set} {m : ℕ} → (eq : EqInst B) → (s : Vec B m) → (v : Vec B (getlen m)) → (h : FinMapMaybe m B) → assoc eq (get (enumerate s)) v ≡ just h → ∃ λ u → bff get eq s v ≡ just u assoc-enough get {B} {m} eq s v h p = map (flip lookup (union h g)) s′ , (begin bff get eq s v ≡⟨ refl ⟩ -- cgit v1.2.3