data TList : List Type -> Type A list of erased (!) types.
This is represents the size of a heterogeneous list (it is just
a natural number at runtime) and is used to split off a
predefined prefix off a heterogeneous list.
Totality: total
Visibility: public export
Constructors:
Nil : TList [](::) : (0 t : Type) -> TList ts -> TList (t :: ts)
splitHList : TList ts -> HList (ts ++ rem) -> (HList ts, HList rem) We can split a concatenation of heterogeneous lists by removing
a fixed-sized prefix.
As a witness of the size of the prefix, a value of type `TList`
is required.
Totality: total
Visibility: public export(++) : TList xs -> TList ys -> TList (xs ++ ys) Concatenates two `TList`s.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7