import Data.String parseNat : String -> Maybe Nat parseNat = parsePositive running_sum : IO Nat running_sum = do putStrLn "enter a number:" stuff <- getLine case parseNat stuff of Nothing => pure 0 (Just n) => map (+n) running_sum in_sequence : List (IO ()) -> IO () in_sequence [] = pure () in_sequence (x::xs) = do x in_sequence xs collect_results : List (IO a) -> IO (List a) collect_results [] = pure [] collect_results (x::xs) = do rx <- x rxs <- collect_results xs pure (rx :: rxs) once_definitely : String -> String -> (String -> Maybe a) -> IO a once_definitely prompt err parse = do putStrLn prompt stuff <- getLine case parse stuff of Nothing => putStrLn err >>= (\_ => once_definitely prompt err parse) (Just x) => pure x ensure_palindrome : Nat -> Maybe Nat ensure_palindrome n = parseNat (reverse (show n)) >>= (\m => if m == n then Just n else Nothing) odd : Nat -> Bool odd Z = False odd (S k) = not (odd k) ensure_odd : Nat -> Maybe Nat ensure_odd n = if odd n then Just n else Nothing -- for the primality test, see the solution to a previous exercise set!