@@ -88,6 +88,18 @@ instance MaxBound (Fin (S n)) where
88 maxBound = last
88 maxBound = last
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')
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')
91-- Construct a Fin from an integer literal which must fit in the given Fin
103-- Construct a Fin from an integer literal which must fit in the given Fin
93natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
105natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
@@ -101,11 +113,12 @@ integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
101integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
113integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
103data IsJust : Maybe a -> Type where
115data IsJust : Maybe a -> Type where
104− ItIsJust : IsJust {a} (Just x)
116+ ItIsJust : IsJust {a} (Just x)
106fromInteger : (x : Integer) ->
118fromInteger : (x : Integer) ->
107− {default ItIsJust
119+ {default ItIsJust
108− prf : (IsJust (integerToFin x n))} -> Fin n
120+ prf : (IsJust (integerToFin x n))} ->
109fromInteger {n} x {prf} with (integerToFin x n)
122fromInteger {n} x {prf} with (integerToFin x n)
110 fromInteger {n} x {prf = ItIsJust} | Just y = y
123 fromInteger {n} x {prf = ItIsJust} | Just y = y