dict.ml

Dictionaries with String-keys. Internally python dicts.

Definitions

Creation

data Dict a

mkDict : List (String, a) -> Dict a

Accessing

dictItems : Dict a -> List (String, a)

dictGet : Dict a -> String -> Maybe a

dictInsert : String -> Dict a -> a -> Dict a