[Agda] collections/containers/finite sets

[Nils Anders Danielsson]

On 2011-11-14 21:30, Arseniy Alekseyev wrote:
> First, after using _×-strictTotalOrder_ or even _×-strictTotalOrder_ I
> get a total order with an equivalence relation different from
> propositional equality. I can't use such a total order with AVL,
> right?

Right. You could in the released version of the library, but I
"simplified" things. Previously lookup had the following type:

   lookup : (k : Key) → Tree → Maybe (∃ λ k′ → Value k′ × k ≈ k′)

Now it has the following type instead:

   lookup : (k : Key) → Tree → Maybe (Value k)

What would you prefer?

Supporting the former type seems to require uglifying the code, so I'm
not too keen on this.

> I can probably replace the equivalence with the equivalent
> propositional equality manually, but still, is there anything to
> facilitate that in the library?

Not off the top of my head. You could define some lemma similar to

   Relation.Binary.Vec.Pointwise.Pointwise-≡.

> Second, the complementary _⊎-isStrictTotalOrder_ seems to be missing.

I added Relation.Binary.Sum._⊎-<-isStrictTotalOrder_.

-- 
/NAD