@@ -56,17 +56,17 @@ instance (Shows k ts) => Show (HVect ts) where
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 { search 100; } p : Elem t ts} -> HVect ts -> t
59+get : {auto p : Elem t ts} -> HVect ts -> t
60get {p = Here} (x::xs) = x
60get {p = Here} (x::xs) = x
61get {p = There p'} (x::xs) = get {p = p'} xs
61get {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 { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts
64+put : {auto p : Elem t ts} -> t -> HVect ts -> HVect ts
65put {p = Here} y (x::xs) = y :: xs
65put {p = Here} y (x::xs) = y :: xs
66put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
66put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
68||| Update an element with the correct type.
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)
69+update : {auto p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
70update {p = Here} f (x::xs) = f x :: xs
70update {p = Here} f (x::xs) = f x :: xs
71update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
71update {p = There p'} f (x::xs) = x :: update {p = p'} f xs