Data.Vect.Binary

The content of this file is taken from the paper
Heterogeneous Binary Random-access lists

Definitions

data BVect : Nat -> Bin -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : BVect n [] a

(::) : IMaybe (isI b) (Tree n a) -> BVect (S n) bs a -> BVect n (b :: bs) a

data Path : Nat -> Bin -> Type

Totality: total
Visibility: public export
Constructors:

Here : Path n -> Path n (I :: bs)

There : Path (S n) bs -> Path n (b :: bs)

zero : Path n (suc bs)

Totality: total
Visibility: public export

lookup : BVect n bs a -> Path n bs -> a

Totality: total
Visibility: public export

cons : Tree n a -> BVect n bs a -> BVect n (suc bs) a

Totality: total
Visibility: public export