Idris2Doc : BinaryRandomAccessList

BinaryRandomAccessList

(source)

Definitions

data BinaryList : Type -> Type
Totality: total
Visibility: export
Constructor: 
BL : List (Digit a) -> BinaryList a

Hint: 
RandomAccessList BinaryList