diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-04-27 20:51:06 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-04-27 20:51:06 +0200 |
| commit | cab5a60cefea9ca03dbdde0a4a33cec20aaeabf6 (patch) | |
| tree | 4376ae6dd79915af1d0d2e7e61c5431d77578b50 | |
| parent | 076752832dbb0989ea4a23a1edca0083db436892 (diff) | |
| download | bidiragda-cab5a60cefea9ca03dbdde0a4a33cec20aaeabf6.tar.gz | |
use fromFunc to define union
Semantically this is no change, but reducing to standard interface seems
better.
| -rw-r--r-- | FinMap.agda | 2 |
1 files changed, 1 insertions, 1 deletions
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)) |