@@ -0,0 +1,16 @@
1+import nat;
2+
3+data Fin : Nat -> Set where
4+ fO : Fin (S k)
5+ | fS : Fin k -> Fin (S k);
6+
7+infixr 7 :: ;
8+
9+data Vect : Set -> Nat -> Set where
10+ VNil : Vect a O
11+ | (::) : a -> Vect a k -> Vect a (S k);
12+
13+vlookup : (i : Fin n) -> Vect a n -> a;
14+vlookup fO (x :: xs) = x;
15+vlookup (fS k) (x :: xs) = vlookup k xs;
16+