@@ -4,6 +4,12 @@ data Fin : Nat -> Set where
44 fO : Fin (S k)
55 | fS : Fin k -> Fin (S k);
66
7+instance Eq (Fin n) where {
8+ fO == fO = True;
9+ (fS k) == (fS k') = k == k';
10+ _ == _ = False;
11+}
12+
713infixr 7 :: ;
814
915data Vect : Set -> Nat -> Set where