TrieOfTrees

Definitions

data Tree : Type -> Type

Totality: total
Visibility: export
Constructors:

E : Tree a

T : a -> Tree a -> Tree a -> Tree a

Hint: 

FiniteMap m k => FiniteMap (Trie (m k)) (Tree k)

data Trie : (Type -> Type) -> Type -> Type -> Type

Totality: not strictly positive
Visibility: export
Constructor: 

MkTrie : Maybe a -> mk (Trie mk ks (Trie mk ks a)) -> Trie mk ks a

Hint: 

FiniteMap m k => FiniteMap (Trie (m k)) (Tree k)