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

jleivent at comcast.net jleivent at comcast.net
Sun Jan 22 17:28:32 CET 2012

>> Thus, I think Jonathan's trick has some right of existence.
>I wouldn't disagree.

Wow.  Erasable encouragement.

Anyway, I do think this trick can be generalized.

-- Jonathan Leivent

More information about the Agda mailing list