[Agda] Erasable vs. irrelevant, and red black trees again

[jleivent at comcast.net]

Here is the red-black tree code I sent in last week, updated (and re-arranged a bit) with this concept of erasable Naturals I've been discussing with you, so that each node in the red-black tree isn't carrying any extra baggage at runtime - just the necessary red/black color flag (and its subtrees, of course).

The bal1 and bal2 functions demonstrate the use of that "weak-disc" axiom.  Comments in bal1 explain the usage.  Hopefully this will clarify things.

Would the black-level terms have been erasable by the compiler had I used normal naturals?  Would the use of the normal "strong" discrimination between zero and suc n for naturals by the type checker when eliminating those impossible cases in bal1 and bal2 have prevented the erasure?

-- Jonathan Leivent
-------------- next part --------------
A non-text attachment was scrubbed...
Name: RB2.zip
Type: application/zip
Size: 8145 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20120120/48fa377f/RB2-0001.zip