@@ -127,6 +127,17 @@ fromInteger : (x : Integer) ->
127fromInteger {n} x {prf} with (integerToFin x n)
127fromInteger {n} x {prf} with (integerToFin x n)
128 fromInteger {n} x {prf = ItIsJust} | Just y = y
128 fromInteger {n} x {prf = ItIsJust} | Just y = y
130+||| Convert an Integer to a Fin in the required bounds/
131+||| This is essentially a composition of `mod` and `fromInteger`
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
139+ {prf = believe_me {a=IsJust (Just val')} ItIsJust}
130%language ErrorReflection
141%language ErrorReflection
132||| Attempt to convert a reflected (fromInteger n) to a Nat
143||| Attempt to convert a reflected (fromInteger n) to a Nat