@@ -347,27 +347,38 @@ natRange n = List.reverse (go n)
347347 where go Z = []
348348 go (S n) = n :: go n
349349
350+-- predifine Nat versions of Enum, so we can use them in the default impls
351+total natEnumFromThen : Nat -> Nat -> Stream Nat
352+natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
353+total natEnumFromTo : Nat -> Nat -> List Nat
354+natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
355+total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
356+natEnumFromThenTo _ Z _ = []
357+natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
358+
350359class Enum a where
351360 total pred : a -> a
352361 total succ : a -> a
362+ succ e = fromNat (S (toNat e))
353363 total toNat : a -> Nat
354364 total fromNat : Nat -> a
355365 total enumFrom : a -> Stream a
356366 enumFrom n = n :: enumFrom (succ n)
357367 total enumFromThen : a -> a -> Stream a
368+ enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
358369 total enumFromTo : a -> a -> List a
370+ enumFromTo x y = map fromNat (natEnumFromTo (toNat x) (toNat y))
359371 total enumFromThenTo : a -> a -> a -> List a
360−
372+ enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
361373
362374instance Enum Nat where
363− pred = Nat.pred
364− succ = S
365− toNat = id
366− fromNat = id
367− enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
368− enumFromThenTo _ Z _ = []
369− enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
370− enumFromTo n m = map (plus n) (natRange ((S m) - n))
375+ pred n = Nat.pred n
376+ succ n = S n
377+ toNat x = id x
378+ fromNat x = id x
379+ enumFromThen x y = natEnumFromThen x y
380+ enumFromThenTo x y z = natEnumFromThenTo x y z
381+ enumFromTo x y = natEnumFromTo x y
371382
372383instance Enum Integer where
373384 pred n = n - 1
@@ -407,6 +418,17 @@ instance Enum Int where
407418 go [] = []
408419 go (x :: xs) = n + (cast x * inc) :: go xs
409420
421+instance Enum (Fin (S n)) where
422+ pred fZ = fZ
423+ pred (fS n) = weaken n
424+ succ n = case strengthen (fS n) of
425+ Left _ => last
426+ Right k => k
427+ toNat n = cast n
428+ fromNat {n=n} m = case natToFin m (S n) of
429+ Just k => k
430+ Nothing => last
431+
410432syntax "[" [start] ".." [end] "]"
411433 = enumFromTo start end
412434syntax "[" [start] "," [next] ".." [end] "]"