@@ -392,13 +392,15 @@ instance Enum Int where
392 succ n = n + 1
392 succ n = n + 1
393 toNat n = cast n
393 toNat n = cast n
394 fromNat n = cast n
394 fromNat n = cast n
397+ then go [] (cast {to = Nat} (m - n)) m
400+ go : List Int -> Nat -> Int -> List Int
401+ go acc Z m = m :: acc
402+ go acc (S k) m = go (m :: acc) k (m - 1)
395 enumFromThen n inc = n :: enumFromThen (inc + n) inc
403 enumFromThen n inc = n :: enumFromThen (inc + n) inc
396− enumFromTo n m = if n <= m
397− then go (natRange (S (cast {to = Nat} (m - n))))
399− where go : List Nat -> List Int
401− go (x :: xs) = n + cast x :: go xs
402 enumFromThenTo _ 0 _ = []
404 enumFromThenTo _ 0 _ = []
403 enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
405 enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
404 where go : List Nat -> List Int
406 where go : List Nat -> List Int