on master help sign in
Minimal Enum instance for Char
e8983e7Gabriel Garcia
libs/prelude/Prelude.idr+6
@@ -203,6 +203,12 @@ instance Enum Int where
203 go [] = []
203 go [] = []
204 go (x :: xs) = n + (cast x * inc) :: go xs
204 go (x :: xs) = n + (cast x * inc) :: go xs
205
205
206+instance Enum Char where
207+ toNat c = toNat (ord c)
208+ fromNat n = chr (fromNat n)
209+
210+ pred c = fromNat (pred (toNat c))
211+
206syntax "[" [start] ".." [end] "]"
212syntax "[" [start] ".." [end] "]"
207 = enumFromTo start end
213 = enumFromTo start end
208syntax "[" [start] "," [next] ".." [end] "]"
214syntax "[" [start] "," [next] ".." [end] "]"