@@ -73,17 +73,17 @@ instance (Shows k ts) => Show (HVect ts) where
7373
7474||| Extract an arbitrary element of the correct type.
7575||| @ t the goal type
76−get : {auto p : Elem t ts} -> HVect ts -> t
77−get {p = Here} (x::xs) = x
78−get {p = There p'} (x::xs) = get {p = p'} xs
76+get : HVect ts -> {auto p : Elem t ts} -> t
77+get (x :: xs) {p = Here} = x
78+get (x :: xs) {p = There p'} = get {p = p'} xs
7979
8080||| Replace an element with the correct type.
81−put : {auto p : Elem t ts} -> t -> HVect ts -> HVect ts
82−put {p = Here} y (x::xs) = y :: xs
83−put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
81+put : t -> HVect ts -> {auto p : Elem t ts} -> HVect ts
82+put y (x::xs) {p = Here} = y :: xs
83+put y (x::xs) {p = There p'} = x :: put {p = p'} y xs
8484
8585||| Update an element with the correct type.
86−update : {auto p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
87−update {p = Here} f (x::xs) = f x :: xs
88−update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
86+update : (t -> u) -> HVect ts -> {auto p : Elem t ts} -> HVect (replaceByElem ts p u)
87+update f (x::xs) {p = Here} = f x :: xs
88+update f (x::xs) {p = There p'} = x :: update {p = p'} f xs
8989