Idris2Doc : Trie

Trie

(source)

Definitions

data Trie : (Type -> Type) -> Type -> Type -> Type
Totality: not strictly positive
Visibility: export
Constructor: 
MkTrie : Maybe a -> mk (Trie mk ks a) -> Trie mk ks a

Hint: 
FiniteMap m k => FiniteMap (Trie (m k)) (List k)