@@ -156,6 +156,14 @@ maximum Z m = m
156156maximum (S n) Z = S n
157157maximum (S n) (S m) = S (maximum n m)
158158
159+||| Tail recursive cast Nat to Int
160+||| Note that this can overflow
161+toIntNat : Nat -> Int
162+toIntNat n = toIntNat' n 0 where
163+ toIntNat' : Nat -> Int -> Int
164+ toIntNat' Z x = x
165+ toIntNat' (S n) x = toIntNat' n (x + 1)
166+
159167--------------------------------------------------------------------------------
160168-- Type class instances
161169--------------------------------------------------------------------------------
@@ -245,9 +253,7 @@ instance Cast Int Nat where
245253 cast i = fromInteger (cast i)
246254
247255instance Cast Nat Int where
248− cast Z = 0
249− cast (S n) = 1 + cast {to=Int} n
250−
256+ cast = toIntNat
251257
252258--------------------------------------------------------------------------------
253259-- Auxilliary notions