@@ -42,7 +42,7 @@ finToNatInjective FZ FZ Refl = Refl
4242finToNatInjective (FS m) FZ Refl impossible
4343finToNatInjective FZ (FS n) Refl impossible
4444finToNatInjective (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))
4646
4747instance Cast (Fin n) Nat where
4848 cast x = finToNat x
@@ -94,7 +94,7 @@ instance Ord (Fin n) where
9494 compare FZ (FS _) = LT
9595 compare (FS _) FZ = GT
9696 compare (FS x) (FS y) = compare x y
97−
97+
9898instance MinBound (Fin (S n)) where
9999 minBound = FZ
100100
@@ -102,24 +102,6 @@ instance MaxBound (Fin (S n)) where
102102 maxBound = last
103103
104104
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−
123105-- Construct a Fin from an integer literal which must fit in the given Fin
124106
125107natToFin : Nat -> (n : Nat) -> Maybe (Fin n)