
  0 | module Syntax.IHateParens.List
  1 | 
  2 | import Data.Vect
  3 | 
  4 | %default total
  5 | 
  6 | public export %inline
  7 | (.length) : List a -> Nat
  8 | xs.length = length xs
  9 | 
 10 | public export %inline
 11 | (.asVect) : (xs : List a) -> Vect xs.length a
 12 | xs.asVect = fromList xs
 13 | 
 14 | public export
 15 | (.withIdx) : (xs : List a) -> List (Fin xs.length, a)
 16 | (.withIdx) []      = []
 17 | (.withIdx) (x::xs) = (FZ, x) :: (xs.withIdx <&> mapFst FS)
 18 |