IdrisのDictionary/Mapのタイプは何ですか

Question

どのように定義できますか？私はその文書に関するこの問題に関する情報は見つけていない。リストとベクトルについてのみ。 contribパッケージで

Answer 1

Data.SortedMapは、通常のインターフェースで、Ordインスタンスを持っているタイプのための有限マップを実装します。

data SortedMap : Type -> Type -> Type 

empty : Ord k => SortedMap k v 
lookup : k -> SortedMap k v -> Maybe v 
insert : k -> v -> SortedMap k v -> SortedMap k v 
delete : k -> SortedMap k v -> SortedMap k v 

fromList : Ord k => List (k, v) -> SortedMap k v 
toList : SortedMap k v -> List (k, v) 

implementation Functor (SortedMap k)