@@ -56,17 +56,17 @@ instance (Shows k ts) => Show (HVect ts) where
5656
5757||| Extract an arbitrary element of the correct type.
5858||| @ t the goal type
59−get : {default tactics { search 100; } p : Elem t ts} -> HVect ts -> t
59+get : {auto p : Elem t ts} -> HVect ts -> t
6060get {p = Here} (x::xs) = x
6161get {p = There p'} (x::xs) = get {p = p'} xs
6262
6363||| Replace an element with the correct type.
64−put : {default tactics { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts
64+put : {auto p : Elem t ts} -> t -> HVect ts -> HVect ts
6565put {p = Here} y (x::xs) = y :: xs
6666put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
6767
6868||| 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)
69+update : {auto p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
7070update {p = Here} f (x::xs) = f x :: xs
7171update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
7272