From 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Tue, 17 Dec 2013 08:49:24 +0100
Subject: refactor to get rid of FinMap without Maybe entirely

The union was the only user of this type and now it uses only partial
mappings. So drop remaining uses of FinMap and make everything work with
FinMapMaybe instead.
---
 BFF.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'BFF.agda')

diff --git a/BFF.agda b/BFF.agda
index f7ddd30..896350a 100644
--- a/BFF.agda
+++ b/BFF.agda
@@ -35,7 +35,7 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where
   bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n))
   bff get s v = let s′ = enumerate s
                     t′ = get s′
-                    g  = partialize (fromFunc (denumerate s))
+                    g  = fromFunc (denumerate s)
                     g′ = delete-many t′ g
                     h  = assoc t′ v
                     h′ = (flip union g′) <$> h
-- 
cgit v1.2.3