@@ -127,6 +127,17 @@ fromInteger : (x : Integer) ->
127127fromInteger {n} x {prf} with (integerToFin x n)
128128 fromInteger {n} x {prf = ItIsJust} | Just y = y
129129
130+||| Convert an Integer to a Fin in the required bounds/
131+||| This is essentially a composition of `mod` and `fromInteger`
132+export
133+restrict : (n : Nat) -> Integer -> Fin (S n)
134+restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
135+ -- reasoning about primitives, so we need the
136+ -- 'believe_me'. It's fine because val' must be
137+ -- in the right range
138+ fromInteger val'
139+ {prf = believe_me {a=IsJust (Just val')} ItIsJust}
140+
130141%language ErrorReflection
131142
132143||| Attempt to convert a reflected (fromInteger n) to a Nat