@@ -368,6 +368,7 @@ instance Enum Nat where
368 toNat = id
368 toNat = id
369 fromNat = id
369 fromNat = id
370 enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
370 enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
371+ enumFromThenTo _ Z _ = []
371 enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S (( m - n) `div` inc)))
372 enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S (( m - n) `div` inc)))
372 enumFromTo n m = map (plus n) (natRange (S (m - n)))
373 enumFromTo n m = map (plus n) (natRange (S (m - n)))
@@ -382,6 +383,7 @@ instance Enum Integer where
382 where go : List Nat -> List Integer
383 where go : List Nat -> List Integer
383 go [] = []
384 go [] = []
384 go (x :: xs) = n + cast x :: go xs
385 go (x :: xs) = n + cast x :: go xs
386+ enumFromThenTo _ 0 _ = []
385 enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))
387 enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))
386 where go : List Nat -> List Integer
388 where go : List Nat -> List Integer
387 go [] = []
389 go [] = []
@@ -397,6 +399,7 @@ instance Enum Int where
397 where go : List Nat -> List Int
399 where go : List Nat -> List Int
398 go [] = []
400 go [] = []
399 go (x :: xs) = n + cast x :: go xs
401 go (x :: xs) = n + cast x :: go xs
402+ enumFromThenTo _ 0 _ = []
400 enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
403 enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
401 where go : List Nat -> List Int
404 where go : List Nat -> List Int
402 go [] = []
405 go [] = []