From cab5a60cefea9ca03dbdde0a4a33cec20aaeabf6 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Fri, 27 Apr 2012 20:51:06 +0200
Subject: use fromFunc to define union

Semantically this is no change, but reducing to standard interface seems
better.
---
 FinMap.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/FinMap.agda b/FinMap.agda
index ff5dda7..fce6384 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -41,7 +41,7 @@ fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMap n A
 fromFunc = tabulate
 
 union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMap n  A → FinMap n A
-union m1 m2 = tabulate (λ f → maybe′ id (lookup f m2) (lookupM f m1))
+union m1 m2 = fromFunc (λ f → maybe′ id (lookup f m2) (lookupM f m1))
 
 restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A
 restrict f is = fromAscList (zip is (map f is))
-- 
cgit v1.2.3