@@ -368,6 +368,7 @@ instance Enum Nat where
368368 toNat = id
369369 fromNat = id
370370 enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
371+ enumFromThenTo _ Z _ = []
371372 enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S (( m - n) `div` inc)))
372373 enumFromTo n m = map (plus n) (natRange (S (m - n)))
373374
@@ -382,6 +383,7 @@ instance Enum Integer where
382383 where go : List Nat -> List Integer
383384 go [] = []
384385 go (x :: xs) = n + cast x :: go xs
386+ enumFromThenTo _ 0 _ = []
385387 enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))
386388 where go : List Nat -> List Integer
387389 go [] = []
@@ -397,6 +399,7 @@ instance Enum Int where
397399 where go : List Nat -> List Int
398400 go [] = []
399401 go (x :: xs) = n + cast x :: go xs
402+ enumFromThenTo _ 0 _ = []
400403 enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
401404 where go : List Nat -> List Int
402405 go [] = []