Safe Haskell	None
Language	Haskell2010

Agda.Utils.IndexMap

Description

Maps from de Bruijn indices, implemented using IntMaps from de Bruijn levels.

Synopsis

Documentation

Maps from de Bruijn indices.

Instances details

Eq a => Eq (IndexMap a) Source #
Instance details Defined in Agda.Utils.IndexMap Methods (==) :: IndexMap a -> IndexMap a -> Bool # (/=) :: IndexMap a -> IndexMap a -> Bool #
Show a => Show (IndexMap a) Source #
Instance details Defined in Agda.Utils.IndexMap Methods showsPrec :: Int -> IndexMap a -> ShowS # show :: IndexMap a -> String # showList :: [IndexMap a] -> ShowS #

The IndexMap invariant.

An empty map.

Inserts a new binding, which will have de Bruijn index 0, and shifts other bindings one step.

Inserts a number of new bindings. The last element in the list will have de Bruijn index 0.

Converts a list to an IndexMap. The last element in the list will have de Bruijn index 0.