PrintBool.agda

module tests.PrintBool where

open import Prelude.IO
open import Prelude.Bool
open import Prelude.Char
open import Prelude.List
open import Prelude.Unit
open import Prelude.String

isNewline : Char -> Bool
isNewline '\n' = true
isNewline _    = false

sequence : {A : Set} -> List (IO A) -> IO (List A)
sequence [] = return []
sequence (x :: xs) =
    r <- x ,
    rs <- sequence xs ,
    return (r :: rs)

mapM : {A B : Set} -> (A -> IO B) -> List A -> IO (List B)
mapM f xs = sequence (map f xs)

printList : List Char -> IO Unit
printList xs = 
  mapM printChar xs ,,
  printChar '\n'


main : IO Unit
main = 
    printChar 'a' ,,
    printList ('a' :: 'b' :: 'c' :: []) ,,
    putStrLn "printBool" ,,
    printBool (isNewline '\n') ,,
    printBool (isNewline 'a') ,,
    return unit