[Agda] finite map
mechvel at botik.ru
Tue Dec 17 09:53:42 CET 2013
On Sat, 2013-12-14 at 20:57 +0400, Sergei Meshveliani wrote:
> 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.
More information about the Agda