search

jfdm / idris-containers

Various data structures for use in the Idris Language.
BSD 3-Clause "New" or "Revised" License
95 stars 21 forks source link

Added slightly modified version of David Christiansen's balance-dependent AVL Tree. #5

Closed ahmadsalim closed 9 years ago

ahmadsalim commented 9 years ago

This is the initial commit of the balance-dependent AVL tree, based on @david-christiansen's work. I have changed the structure such that it is parameterized by its Ord instance to ensure coherency, and changed the height function to allow easier proofs.

ahmadsalim commented 9 years ago

There are still some essential operations missing such as remove, and the merging/splitting operations. I have uploaded it to allow for testing and gradual implementation of the rest of the operations, and to allow other interested parties like @markuspf to modify the things they want.