@@ -365,9 +365,8 @@ instance Enum Nat where
365 fromNat = id
365 fromNat = id
366 enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
366 enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
367 enumFromThenTo _ Z _ = []
367 enumFromThenTo _ Z _ = []
368− enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S (( m - n) `div` inc)))
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)))
369+ enumFromTo n m = map (plus n) (natRange ((S m) - n))
372instance Enum Integer where
371instance Enum Integer where
373 pred n = n - 1
372 pred n = n - 1
@@ -375,7 +374,9 @@ instance Enum Integer where
375 toNat n = cast n
374 toNat n = cast n
376 fromNat n = cast n
375 fromNat n = cast n
377 enumFromThen n inc = n :: enumFromThen (inc + n) inc
376 enumFromThen n inc = n :: enumFromThen (inc + n) inc
377+ enumFromTo n m = if n <= m
378− enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
378+ then go (natRange (S (cast {to = Nat} (m - n))))
379 where go : List Nat -> List Integer
380 where go : List Nat -> List Integer
380 go [] = []
381 go [] = []
381 go (x :: xs) = n + cast x :: go xs
382 go (x :: xs) = n + cast x :: go xs
@@ -391,7 +392,9 @@ instance Enum Int where
391 toNat n = cast n
392 toNat n = cast n
392 fromNat n = cast n
393 fromNat n = cast n
393 enumFromThen n inc = n :: enumFromThen (inc + n) inc
394 enumFromThen n inc = n :: enumFromThen (inc + n) inc
395+ enumFromTo n m = if n <= m
394− enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
396+ then go (natRange (S (cast {to = Nat} (m - n))))
395 where go : List Nat -> List Int
398 where go : List Nat -> List Int
396 go [] = []
399 go [] = []
397 go (x :: xs) = n + cast x :: go xs
400 go (x :: xs) = n + cast x :: go xs