@@ -42,4 +42,27 @@ last {n=O} = fO
4242last {n=S _} = fS last
4343
4444total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
45−fSinjective refl = refl
45+fSinjective refl = refl
46+
47+
48+-- Construct a Fin from an integer literal which must fit in the given Fin
49+
50+natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
51+natToFin O (S j) = Just fO
52+natToFin (S k) (S j) with (natToFin k j)
53+ | Just k' = Just (fS k')
54+ | Nothing = Nothing
55+natToFin _ _ = Nothing
56+
57+integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
58+integerToFin x = natToFin (cast x)
59+
60+data IsJust : Maybe a -> Type where
61+ ItIsJust : IsJust {a} (Just x)
62+
63+fromInteger : (x : Integer) ->
64+ {default (ItIsJust _ _)
65+ prf : (IsJust (integerToFin x n))} -> Fin n
66+fromInteger {n} x {prf} with (integerToFin x n)
67+ fromInteger {n} x {prf = ItIsJust} | Just y = y
68+