15 lines
433 B
Plaintext
15 lines
433 B
Plaintext
|
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
|