git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2600 from david-christiansen/no-more-fin-plus
d03c71cDavid Christiansen
CHANGELOG+1
compare with master
unifiedsplit
@@ -22,6 +22,7 @@ such, the (-) operator and 'abs' have been moved there from 'Num'.
22* A special version of (-) on 'Nat' requires that the second argument is
22* A special version of (-) on 'Nat' requires that the second argument is
23smaller than or equal to the first. 'minus' retains the old behaviour,
23smaller than or equal to the first. 'minus' retains the old behaviour,
24returning Z if there is an underflow.
24returning Z if there is an underflow.
25+* The (+), (-), and (*) operations on Fin have been removed.
25* New Logging Effects have been added to facilitate logging of effectful
26* New Logging Effects have been added to facilitate logging of effectful
26 programmes.
27 programmes.
27
28
libs/base/Data/Fin.idr+2−20
@@ -42,7 +42,7 @@ finToNatInjective FZ FZ Refl = Refl
42finToNatInjective (FS m) FZ Refl impossible
42finToNatInjective (FS m) FZ Refl impossible
43finToNatInjective FZ (FS n) Refl impossible
43finToNatInjective FZ (FS n) Refl impossible
44finToNatInjective (FS m) (FS n) prf =
44finToNatInjective (FS m) (FS n) prf =
45− cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
45+ cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))
46
46
47instance Cast (Fin n) Nat where
47instance Cast (Fin n) Nat where
48 cast x = finToNat x
48 cast x = finToNat x
@@ -94,7 +94,7 @@ instance Ord (Fin n) where
94 compare FZ (FS _) = LT
94 compare FZ (FS _) = LT
95 compare (FS _) FZ = GT
95 compare (FS _) FZ = GT
96 compare (FS x) (FS y) = compare x y
96 compare (FS x) (FS y) = compare x y
97−
97+
98instance MinBound (Fin (S n)) where
98instance MinBound (Fin (S n)) where
99 minBound = FZ
99 minBound = FZ
100
100
@@ -102,24 +102,6 @@ instance MaxBound (Fin (S n)) where
102 maxBound = last
102 maxBound = last
103
103
104
104
105−||| Add two Fins, extending the bound
106−(+) : Fin n -> Fin m -> Fin (n + m)
107−(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
108−(+) (FS f) f' = FS (f + f')
109−
110−||| Substract two Fins, keeping the bound of the minuend
111−(-) : Fin n -> Fin m -> Fin n
112−FZ - _ = FZ
113−f - FZ = f
114−(FS f) - (FS f') = weaken $ f - f'
115−
116−||| Multiply two Fins, extending the bound
117−(*) : Fin n -> Fin m -> Fin (n * m)
118−(*) {n=Z} f f' = FinZElim f
119−(*) {m=Z} f f' = FinZElim f'
120−(*) {n=S n} {m=S m} FZ f' = FZ
121−(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')
122−
123-- Construct a Fin from an integer literal which must fit in the given Fin
105-- Construct a Fin from an integer literal which must fit in the given Fin
124
106
125natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
107natToFin : Nat -> (n : Nat) -> Maybe (Fin n)