git.iko.soy/Idris-dev
on master help sign in
Equality on Fin
72c2e2aEdwin Brady
lib/vect.idr+6
compare with master
unifiedsplit
@@ -4,6 +4,12 @@ data Fin : Nat -> Set where
4 fO : Fin (S k)
4 fO : Fin (S k)
5 | fS : Fin k -> Fin (S k);
5 | fS : Fin k -> Fin (S k);
6
6
7+instance Eq (Fin n) where {
8+ fO == fO = True;
9+ (fS k) == (fS k') = k == k';
10+ _ == _ = False;
11+}
12+
7infixr 7 :: ;
13infixr 7 :: ;
8
14
9data Vect : Set -> Nat -> Set where
15data Vect : Set -> Nat -> Set where