git.iko.soy/Idris-dev
on master help sign in
/= for Fin
commit04ac1a8047db838c9f2d15cd80237bdb642d9920 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 17 Nov 2011, 13:52 (15 years ago) parent72c2e2a
1 file changed+2
compare with master
unifiedsplit
lib/vect.idr+2
lib/vect.idr+2
@@ -8,6 +8,8 @@ instance Eq (Fin n) where {
88 fO == fO = True;
99 (fS k) == (fS k') = k == k';
1010 _ == _ = False;
11+
12+ x /= y = not (x == y);
1113}
1214
1315infixr 7 :: ;