[Agda] collections/containers/finite sets

[Nils Anders Danielsson]

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