Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Utils.Trie

Synopsis

- data Trie k v
- empty :: Trie k v
- singleton :: [k] -> v -> Trie k v
- insert :: Ord k => [k] -> v -> Trie k v -> Trie k v
- lookupPath :: Ord k => [k] -> Trie k v -> [v]
- union :: Ord k => Trie k v -> Trie k v -> Trie k v

# Documentation

data Trie k v

Instances

(Show k, Show v) => Show (Trie k v) |

empty :: Trie k v

singleton :: [k] -> v -> Trie k v

insert :: Ord k => [k] -> v -> Trie k v -> Trie k v

lookupPath :: Ord k => [k] -> Trie k v -> [v]

union :: Ord k => Trie k v -> Trie k v -> Trie k v

Left biased union.