@@ -392,13 +392,15 @@ instance Enum Int where
392392 succ n = n + 1
393393 toNat n = cast n
394394 fromNat n = cast n
395+ enumFromTo n m =
396+ if n <= m
397+ then go [] (cast {to = Nat} (m - n)) m
398+ else []
399+ where
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)
395403 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))))
398− else []
399− where go : List Nat -> List Int
400− go [] = []
401− go (x :: xs) = n + cast x :: go xs
402404 enumFromThenTo _ 0 _ = []
403405 enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
404406 where go : List Nat -> List Int