@@ -52,21 +52,21 @@ using (k : Nat, ts : Vect k Type)
5252 shows (x::xs) = show x :: shows xs
5353
5454 instance (Shows k ts) => Show (HVect ts) where
55− show xs = show (shows xs)
55+ show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"
5656
5757 ||| Extract an arbitrary element of the correct type.
5858 ||| @ t the goal type
59− get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
59+ get : {default tactics { search 100; } p : Elem t ts} -> HVect ts -> t
6060 get {p = Here} (x::xs) = x
6161 get {p = There p'} (x::xs) = get {p = p'} xs
6262
6363 ||| Replace an element with the correct type.
64− put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
64+ put : {default tactics { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts
6565 put {p = Here} y (x::xs) = y :: xs
6666 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
6767
68− ||| Replace an element with the correct type.
69− update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
68+ ||| Update an element with the correct type.
69+ update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
7070 update {p = Here} f (x::xs) = f x :: xs
7171 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
7272