@@ -365,9 +365,8 @@ instance Enum Nat where
365365 fromNat = id
366366 enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
367367 enumFromThenTo _ Z _ = []
368− enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S (( m - n) `div` inc)))
369− enumFromTo n m = map (plus n) (natRange (S (m - n)))
370−
368+ enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
369+ enumFromTo n m = map (plus n) (natRange ((S m) - n))
371370
372371instance Enum Integer where
373372 pred n = n - 1
@@ -375,7 +374,9 @@ instance Enum Integer where
375374 toNat n = cast n
376375 fromNat n = cast n
377376 enumFromThen n inc = n :: enumFromThen (inc + n) inc
378− enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
377+ enumFromTo n m = if n <= m
378+ then go (natRange (S (cast {to = Nat} (m - n))))
379+ else []
379380 where go : List Nat -> List Integer
380381 go [] = []
381382 go (x :: xs) = n + cast x :: go xs
@@ -391,7 +392,9 @@ instance Enum Int where
391392 toNat n = cast n
392393 fromNat n = cast n
393394 enumFromThen n inc = n :: enumFromThen (inc + n) inc
394− enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
395+ enumFromTo n m = if n <= m
396+ then go (natRange (S (cast {to = Nat} (m - n))))
397+ else []
395398 where go : List Nat -> List Int
396399 go [] = []
397400 go (x :: xs) = n + cast x :: go xs