@@ -88,6 +88,18 @@ instance MaxBound (Fin (S n)) where
8888 maxBound = last
8989
9090
91+||| Add two Fins, extending the bound
92+(+) : Fin n -> Fin m -> Fin (n + m)
93+(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
94+(+) (fS f) f' = fS (f + f')
95+
96+||| Multiply two Fins, extending the bound
97+(*) : Fin n -> Fin m -> Fin (n * m)
98+(*) {n=Z} f f' = FinZElim f
99+(*) {m=Z} f f' = FinZElim f'
100+(*) {n=S n} {m=S m} fZ f' = fZ
101+(*) {n=S n} {m=S m} (fS f) f' = f' + (f * f')
102+
91103-- Construct a Fin from an integer literal which must fit in the given Fin
92104
93105natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
@@ -101,11 +113,12 @@ integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
101113integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
102114
103115data IsJust : Maybe a -> Type where
104− ItIsJust : IsJust {a} (Just x)
116+ ItIsJust : IsJust {a} (Just x)
105117
106118fromInteger : (x : Integer) ->
107− {default ItIsJust
108− prf : (IsJust (integerToFin x n))} -> Fin n
119+ {default ItIsJust
120+ prf : (IsJust (integerToFin x n))} ->
121+ Fin n
109122fromInteger {n} x {prf} with (integerToFin x n)
110123 fromInteger {n} x {prf = ItIsJust} | Just y = y
111124