Purely Functional Data Structures in Idris

This is a collection of purely functional data structures implemented in Idris, some of them adapted from Chris Okasaki's book. Where possible, I tried to use size-indexed types.

Compatibility: Requires Idris >= 0.11