Skip to content

Latest commit

 

History

History

depending-on-types

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
Okasaki.hs
Okasaki.hs
 
 
Ordering.agda
Ordering.agda
 
 
RBT.agda
RBT.agda
 
 
RBT.hs
RBT.hs
 
 
README.md
README.md
 
 
SimpleRBT.hs
SimpleRBT.hs
 
 

README.md

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