[Agda] finite map

[Sergei Meshveliani]

On Sat, 2013-12-14 at 20:57 +0400, Sergei Meshveliani wrote:
> People,
> I have   A : Setoid α α=,  aC = Setoid.Carrier A,  B : Setoid β β=,
>          bC = Setoid.Carrier B,
> 
> and need to operate with finite maps  f : aC → bC :
> 
> membership, lookup, insertion, union, equality.
> O(n) lookup/insert  is sufficient, so far.

I consider implementing  AssociationList,
like AssocList in the Haskell library, only with some proofs.

Has the Agda standard library such? 


> Need I to add a number  i : ℕ,  to make pairs  (x , i) : aC × ℕ
> compared _<_  by  i,  and to use  AVL  over the TotalOrder key domain of
> aC × ℕ
> ?

The idea was that _≡_ on  ℕ × aC  to support operating with  _≈_ on aC
(as Data.AVL relies on _≡_).
But probably, this is an error.

Thanks,

------
Sergei