This project provides an implementation of infinite-length lists that aims to improve on: Data.Stream by offering a O(lg n) bound for (!!) Data.Sequence by allowing lists to be infinite. Unfortunately, cons is an O(lg k) (where k elements of the stream are eventually forced) operation, while is it O(1) on regular lists, Data.Sequences, and Data.Streams. The internal representation uses Braun trees (or Braun streams, in this case). The latest API documentation is here. The Coq proofs are here.