Change to infix form
commit7800e3c91fa67e88eee0734dcaab453d9637b976
authorJean-Remi Desjardins <jeanremi.desjardins@gmail.com>
dateWed 26 Mar 2014, 14:40 (13 years ago)
parent70597fa
libs/prelude/Prelude/Fin.idr+3−3
@@ -95,9 +95,9 @@ instance MaxBound (Fin (S n)) where
9595
9696||| Substract two Fins, keeping the bound of the minuend
9797(-) : Fin n -> Fin m -> Fin n
98−(-) fZ _ = fZ
99−(-) f fZ = f
100−(-) (fS f) (fS f') = weaken $ f - f'
98+fZ - _ = fZ
99+f - fZ = f
100+(fS f) - (fS f') = weaken $ f - f'
101101
102102||| Multiply two Fins, extending the bound
103103(*) : Fin n -> Fin m -> Fin (n * m)