[Agda] collections/containers/finite sets

[Arseniy Alekseyev]

Dear Nils,

I have tried AVL from the latest version of the library and have some questions.

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? I can probably replace the equivalence with the equivalent
propositional equality manually, but still, is there anything to
facilitate that in the library?

Second, the complementary _⊎-isStrictTotalOrder_ seems to be missing.
What are the best components to concoct it from? Should I try using
non-strict total order machinery, or will it be easier to implement it
from scratch (especially considering the prop. equality problem)?

That's all for now.
Thank you for the library!
Arseniy.

On 14 November 2011 12:28, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-11-14 13:03, Ramana Kumar wrote:
>>
>> record TypeOperator : Set where
>>   field name  : String
>>         arity : ℕ
>>
>> data Type : Set where
>>   TyVar : String ->  Type
>>   TyApp : (op : TypeOperator) ->  Vec Type (TypeOperator.arity op) ->
>>  Type
>>
>> Now suppose I want to make AVL Sets of these Types.
>> That should require me to come up with a strict total order on them,
>> right?
>> But I would imagine that such a relation can be computed completely
>> automatically using existing relations on String and Vec.
>> What's the best (i.e. shortest, or most elegant) way to continue this
>> module so it eventually includes a value whose type is an AVL set of
>> Types?
>
> If you want to combine two strict total orders into one you can use
>
>  Relation.Binary.Product.StrictLex._×-strictTotalOrder_,
>
> and for lists you can use
>
>  Relation.Binary.List.StrictLex.<-strictTotalOrder.
>
> The library does not define a strict total order for strings, but you
> can define one by converting the strings to lists of natural numbers.
>
> --
> /NAD
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>