[Agda] DTO, STO, AVL.Tree

[Nils Anders Danielsson]

On 2012-10-19 21:49, Serge D. Mechveliani wrote:
> 1. The `class'  Setoid,  with its fields  Carrier  and  \~~.
>     I think,  \~~  needs to be used as the algebraic equality,
>     similarly as  (==) used in Haskell.

I don't know what you mean by algebraic equality. Note that

   _≈_ : Carrier → Carrier → Set <something>,

whereas (==) is boolean-valued.

> I am not sure, but have an impression that
> 1) STO needs to be removed and to merge to DTO, with _<_ defined via
>     _<=_  and  \neg (x \~~ y),

See Relation.Binary.Props.StrictTotalOrder and
Relation.Binary.Props.DecTotalOrder.

> 2) AVL needs to generalize from \equiv to \~~.

A previous version of Data.AVL allowed arbitrary equivalence relations.
When I added the search tree invariant to the data structure I switched
to a less general interface in order to avoid some complications. We
could switch back, but I believe that both the code and the interface
would become more complicated.

-- 
/NAD