use fromFunc to define union
authorHelmut Grohne <helmut@subdivi.de>
Fri, 27 Apr 2012 18:51:06 +0000 (20:51 +0200)
committerHelmut Grohne <helmut@subdivi.de>
Fri, 27 Apr 2012 18:51:06 +0000 (20:51 +0200)
Semantically this is no change, but reducing to standard interface seems
better.

FinMap.agda

index ff5dda7..fce6384 100644 (file)
@@ -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))