git.iko.soy/Idris-dev
on master help sign in
/= for Fin
04ac1a8Edwin Brady
lib/vect.idr+2
compare with master
unifiedsplit
@@ -8,6 +8,8 @@ instance Eq (Fin n) where {
8 fO == fO = True;
8 fO == fO = True;
9 (fS k) == (fS k') = k == k';
9 (fS k) == (fS k') = k == k';
10 _ == _ = False;
10 _ == _ = False;
11+
12+ x /= y = not (x == y);
11}
13}
12
14
13infixr 7 :: ;
15infixr 7 :: ;