[Agda] red black trees with delete

[Nils Anders Danielsson]

On 2012-01-11 03:36, jleivent at comcast.net wrote:
> Since I'm a novice at dependent-typed programming, I'm not sure if
> this is a trivial result or not. However, one interesting thing is
> that I didn't previously know or refer to any existing red black tree
> implementation of delete - I just allowed the combination of the Agda
> type checker and the exacting dependent type signatures to do their
> thing (with some simple reasoning about what the delete function must
> contain - such as a delete minimum function) - making me feel more
> like a facilitator than a programmer.

I had a similar experience when implementing the AVL trees in the
standard library. I had never implemented tree rotations, but once I had
the types in place (at that time primarily balancing information) the
rotations almost wrote themselves.

-- 
/NAD