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