[Agda] finite map

Sergei Meshveliani mechvel at botik.ru
Sat Dec 14 17:57:55 CET 2013

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.

Has Standard library something ready for this?

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 × ℕ
(one can consider Bin instead of ℕ).



More information about the Agda mailing list