bimap package:Agda
Partly invertible finite maps.
Time complexities are given under the assumption that all relevant
instance functions, as well as arguments of function type, take
constant time, and "n" is the number of keys involved in the
operation.
Finite maps from
k to
v, with a way to quickly get
from
v to
k for certain values of type
v
(those for which
tag is defined).
Every value of this type must satisfy
biMapInvariant.