2022-09-28 23:04:00 +00:00
|
|
|
module Map where
|
|
|
|
|
|
|
|
|
|
-- not really used yet
|
|
|
|
|
|
2022-09-28 04:12:48 +00:00
|
|
|
record Map (K V : Set) : Set where
|
|
|
|
|
constructor mapOf
|
|
|
|
|
field
|
|
|
|
|
keys : List K
|
|
|
|
|
values : List V
|
|
|
|
|
|
|
|
|
|
showMap : {V : Set} → (V → String) → Map String V → String
|
|
|
|
|
showMap f m = "map: " +++ (showList ident (zip (Map.keys m) (map f (Map.values m))))
|
|
|
|
|
|
|
|
|
|
findMap : Map Nat Nat → Nat → Nat
|
|
|
|
|
findMap m k = takeIndex 0 (Map.values m) (findIndex 0 k (Map.keys m))
|
|
|
|
|
|
|
|
|
|
showNatMap : Map String Nat → String
|
|
|
|
|
showNatMap m = showMap show m
|
