Idris2Doc : AltBinaryRandomAccessList

AltBinaryRandomAccessList

(source)

Definitions

data BinaryList : Type -> Type
Totality: total
Visibility: export
Constructors:
Nil : BinaryList a
Zero : BinaryList (a, a) -> BinaryList a
One : a -> BinaryList (a, a) -> BinaryList a

Hint: 
RandomAccessList BinaryList