@@ -52,21 +52,21 @@ using (k : Nat, ts : Vect k Type)
52 shows (x::xs) = show x :: shows xs
52 shows (x::xs) = show x :: shows xs
54 instance (Shows k ts) => Show (HVect ts) where
54 instance (Shows k ts) => Show (HVect ts) where
55− show xs = show (shows xs)
55+ show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"
57 ||| Extract an arbitrary element of the correct type.
57 ||| Extract an arbitrary element of the correct type.
58 ||| @ t the goal type
58 ||| @ 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
60 get {p = Here} (x::xs) = x
60 get {p = Here} (x::xs) = x
61 get {p = There p'} (x::xs) = get {p = p'} xs
61 get {p = There p'} (x::xs) = get {p = p'} xs
63 ||| Replace an element with the correct type.
63 ||| 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
65 put {p = Here} y (x::xs) = y :: xs
65 put {p = Here} y (x::xs) = y :: xs
66 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
66 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
68− ||| Replace an element with the correct type.
68+ ||| Update 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)
69+ update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
70 update {p = Here} f (x::xs) = f x :: xs
70 update {p = Here} f (x::xs) = f x :: xs
71 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
71 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs