idris-0.11.1: test/totality012/totality012a.idr

%default total

data InfIO : Type -> Type where
     PutStr : String -> InfIO ()
     GetStr : InfIO String
     (>>=) : InfIO a -> (a -> Inf (InfIO b)) -> InfIO b

echo2 : String -> InfIO ()
echo2 x = case (x == "quit") of
               True => PutStr "Bye!\n"
               False => echo2 x