From 20c176d383e59a0345f7425c5f14679906159a59 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 4 Feb 2014 10:52:49 +0100
Subject: add convenience members to PartialVecVec.Get

---
 BFF.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'BFF.agda')

diff --git a/BFF.agda b/BFF.agda
index 5bf756d..f5573ba 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -38,7 +38,7 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate = flip lookupV
 
 
-  bff : (G : Get) → ({i : Setoid.Carrier (Get.I G)} → Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i) → Vec Carrier ((Get.gl₂ G) ⟨$⟩ i) → Maybe (Vec Carrier (to (Get.gl₁ G) ⟨$⟩ i)))
+  bff : (G : Get) → ({i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i)))
   bff G s v = let   s′ = enumerate s
                     t′ = Get.get G s′
                     g  = fromFunc (denumerate s)
-- 
cgit v1.2.3