ucsd-progsys/liquidhaskell — pull request #282 by michaelbeaumont (2014-12-08 23:23:58+00:00)
Title: Completed (insertion at least) AVL implementation, passes the totality checker

I kept the proofs for the rebalance functions just as examples.