[Agda] collections/containers/finite sets

[Arseniy Alekseyev]

> 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?

I only need the latter right now and it looks much nicer.
However, because we don't have extensionality/quotient types, someone
will eventually need the former.
Anyway, you probably know all the pros and cons much better than I do.

Thanks for the tips.

Arseniy.

On 15 November 2011 15:55, Nils Anders Danielsson <nad at chalmers.se> wrote:
> 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?
>
>
> 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
>
>