This is an Idris port of the Haskell code from Appendix A of "Purely Functional Data Structures", by Chris Okasaki. As such, it might be considered a derivative work. If so, Cambridge University Press holds the copyright to the original work. This work was produced without the knowledge, permissions, or assistance of Cambridge University Press. The author(s) of this work do not consider it a derivative work, but will make every effort to cease publication as the request of any of the original copyright holder(s) or Chris Okasaki.

Any errors introduced by the port were introduced by its authors, and are neither the responsibility of nor should poorly reflect on "Purely Functional Data Structures", its copyright holders, or Chris Okasaki. Error reports are appreciated.

To discourage any action from other copyright claimants, encourage maximum distribution, and recognize the essentially shared nature of any work on such fundamental data structures, the author(s) have chosen the most permissive of licenses--CC0--a copy of which should be available in the LICENSE.CC0 file distributed with this work and can be found at https://creativecommons.org/publicdomain/zero/1.0/