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

Safe HaskellNone
LanguageHaskell98

Agda.Utils.BiMap

Contents

Description

Finite bijections (implemented as a pair of maps).

Synopsis

Documentation

data BiMap a b Source

Finite bijective map from a to b. There, and back again.

Constructors

BiMap 

Fields

biMapThere :: Map a b
 
biMapBack :: Map b a
 

Instances

(Ord a, Ord b) => Eq (BiMap a b) Source 
(Ord a, Ord b) => Ord (BiMap a b) Source 
(Show a, Show b, Ord a, Ord b) => Show (BiMap a b) Source 
(Ord a, Ord b, Arbitrary a, Arbitrary b) => Arbitrary (BiMap a b) Source 
(Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) Source 

lookup :: (Ord a, Ord b) => a -> BiMap a b -> Maybe b Source

Lookup. O(log n).

invLookup :: (Ord a, Ord b) => b -> BiMap a b -> Maybe a Source

Inverse lookup. O(log n).

empty :: (Ord a, Ord b) => BiMap a b Source

Empty bimap. O(1).

singleton :: (Ord a, Ord b) => a -> b -> BiMap a b Source

Singleton bimap. O(1).

insert :: (Ord a, Ord b) => a -> b -> BiMap a b -> BiMap a b Source

Insert. Overwrites existing value if present.

union :: (Ord a, Ord b) => BiMap a b -> BiMap a b -> BiMap a b Source

Left-biased Union. O(Map.union).

fromList :: (Ord a, Ord b) => [(a, b)] -> BiMap a b Source

Construct from a list of pairs.

Does not check for actual bijectivity of constructed finite map.

toList :: (Ord a, Ord b) => BiMap a b -> [(a, b)] Source

Turn into list, sorted ascendingly by first value.

Instances

Properties

All tests