Idris2Doc : Data.Vect.Binary

Data.Vect.Binary

The content of this file is taken from the paper
Heterogeneous Binary Random-access lists
dataBVect : Nat -> Bin -> Type -> Type
Totality: total
Constructors:
Nil : BVectn [] a
(::) : IMaybe (isIb) (Treena) -> BVect (Sn) bsa -> BVectn (b::bs) a
dataPath : Nat -> Bin -> Type
Totality: total
Constructors:
Here : Pathn -> Pathn (I::bs)
There : Path (Sn) bs -> Pathn (b::bs)
cons : Treena -> BVectnbsa -> BVectn (sucbs) a
Totality: total
lookup : BVectnbsa -> Pathnbs -> a
Totality: total
zero : Pathn (sucbs)
Totality: total