@@ -156,6 +156,14 @@ maximum Z m = m
156maximum (S n) Z = S n
156maximum (S n) Z = S n
157maximum (S n) (S m) = S (maximum n m)
157maximum (S n) (S m) = S (maximum n m)
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
165+ toIntNat' (S n) x = toIntNat' n (x + 1)
159--------------------------------------------------------------------------------
167--------------------------------------------------------------------------------
160-- Type class instances
168-- Type class instances
161--------------------------------------------------------------------------------
169--------------------------------------------------------------------------------
@@ -245,9 +253,7 @@ instance Cast Int Nat where
245 cast i = fromInteger (cast i)
253 cast i = fromInteger (cast i)
247instance Cast Nat Int where
255instance Cast Nat Int where
248− cast Z = 0
256+ cast = toIntNat
249− cast (S n) = 1 + cast {to=Int} n
252--------------------------------------------------------------------------------
258--------------------------------------------------------------------------------
253-- Auxilliary notions
259-- Auxilliary notions