[Agda] finite map
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