[Agda] red black trees with delete

[Andreas Abel]

Hello Jonathan,

you might be interested to compare your solution to Julien Oster's.

   https://bitbucket.org/anyfoo/agda-std-trees/src

Cheers,
Andreas

On 1/11/12 2:04 PM, Nils Anders Danielsson wrote:
> 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.
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/