@@ -0,0 +1,16 @@
3+data Fin : Nat -> Set where
5+ | fS : Fin k -> Fin (S k);
9+data Vect : Set -> Nat -> Set where
11+ | (::) : a -> Vect a k -> Vect a (S k);
13+vlookup : (i : Fin n) -> Vect a n -> a;
14+vlookup fO (x :: xs) = x;
15+vlookup (fS k) (x :: xs) = vlookup k xs;