Examples from "Depending on Types"
-
Okasaki.hs Chris Okasaki's 1993 functional pearl: insertion into red black trees
-
RBT.agda An Agda version that shows that insertion preserves the color and height invariants (modified from code by Dan Licata).
-
RBT.hs A Haskell translation of the Agda code
-
SimpleRBT.hs A different Haskell solution, where totality reasoning is more difficult