This packages provides containers not defined in Idris `base`, `prelude`, or `contrib` and are for use in Idris programmes. They are built:
primarily with existence in mind rather than a dependently typed construction. The latter of which may come later.
If you would like to contribute please see CONTRIBUTING.md that offers some guidance. At the moment I am doing some work in the dev branch and master is the stable version.
The ordered motivation behind these data structures are:
- My work requires the use of data structures that may not already be in the
Idrisbase package. - I do not like the implementation of a certain container and am providing an alternate construction.
- An exercise in implementing different data structures using functional programming.
- An exercise in using dependent types to implement different data structures.
- AVL Tree implementations of:
- Tree.
- Dictionary.
- Set.
- Graphs using Adjacency Lists.
- Stack Based Queue
- List based Stack
- Dependently Typed AVL tree.
The containers built here are rough and ready. They may fail; they may not work as intended. There will be code duplication, there may not be documentation.
If there is something missing, that you would like to see please contribute. I welcome reasonable PR and changes to design.
There is a rudimentary testing suite that needs extending, and checks of the implementation’s need performing. There is a quickcheck port to Idris out there but it may have bit-rotten away.
Also please read the CONTRIBUTING.md guidelines, for everyone’s sanity.