
 0 | module FiniteMap
 1 | 
 2 | %default total
 3 | 
 4 | public export
 5 | interface FiniteMap (m : Type -> Type -> Type) k where
 6 |   empty : m k a
 7 |   bind : k -> a -> m k a -> m k a
 8 |   lookup : k -> m k a -> Maybe a
 9 |