Idris2Doc : Data.Vect.Binary

Data.Vect.Binary

The content of this file is taken from the paper
Heterogeneous Binary Random-access lists
data BVect : Nat -> Bin -> Type -> Type
Totality: total
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
Constructors:
Here : Path n -> Path n (I :: bs)
There : Path (S n) bs -> Path n (b :: bs)
cons : Tree n a -> BVect n bs a -> BVect n (suc bs) a
Totality: total
lookup : BVect n bs a -> Path n bs -> a
Totality: total
zero : Path n (suc bs)
Totality: total