@@ -6,7 +6,8 @@ import Data.Vect
66%default total
77
88using (k : Nat, ts : Vect k Type)
9− ||| Heterogeneous vectors where the type index gives, element-wise, the types of the contents
9+ ||| Heterogeneous vectors where the type index gives, element-wise,
10+ ||| the types of the contents.
1011 data HVect : Vect k Type -> Type where
1112 Nil : HVect []
1213 (::) : t -> HVect ts -> HVect (t::ts)
@@ -30,6 +31,7 @@ using (k : Nat, ts : Vect k Type)
3031 updateAt fZ f (x::xs) = f x :: xs
3132 updateAt (fS j) f (x::xs) = x :: updateAt j f xs
3233
34+ ||| Append two `HVect`s.
3335 (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)
3436 (++) [] ys = ys
3537 (++) (x::xs) ys = x :: (xs ++ ys)
@@ -52,16 +54,18 @@ using (k : Nat, ts : Vect k Type)
5254 instance (Shows k ts) => Show (HVect ts) where
5355 show xs = show (shows xs)
5456
55− ||| Extract an arbitrary element of the correct type
57+ ||| Extract an arbitrary element of the correct type.
5658 ||| @ t the goal type
5759 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
5860 get {p = Here} (x::xs) = x
5961 get {p = There p'} (x::xs) = get {p = p'} xs
6062
63+ ||| Replace an element with the correct type.
6164 put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
6265 put {p = Here} y (x::xs) = y :: xs
6366 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
6467
68+ ||| Replace an element with the correct type.
6569 update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
6670 update {p = Here} f (x::xs) = f x :: xs
6771 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs