Control.RIO.Console

Definitions

record ConsoleOut : Type

  Record representing a console with
  standard output and error output

Totality: total
Visibility: public export
Constructor: 

MkConsoleOut : (String -> IO ()) -> (String -> IO ()) -> ConsoleOut

Projections:

.putErr_ : ConsoleOut -> String -> IO ()

.putStr_ : ConsoleOut -> String -> IO ()

Hint: 

Console -> ConsoleOut

.putStr_ : ConsoleOut -> String -> IO ()

Totality: total
Visibility: public export

putStr_ : ConsoleOut -> String -> IO ()

Totality: total
Visibility: public export

.putErr_ : ConsoleOut -> String -> IO ()

Totality: total
Visibility: public export

putErr_ : ConsoleOut -> String -> IO ()

Totality: total
Visibility: public export

stdOut : ConsoleOut

  The default console, printing to standard out and standard err.

Totality: total
Visibility: export

cputStr : ConsoleOut => HasIO io => String -> io ()

  Put a string to the console's standard output.

Totality: total
Visibility: export

cputStrLn : ConsoleOut => HasIO io => String -> io ()

  Put a string plus trailing line break
  to the console's standard output.

Totality: total
Visibility: export

cprint : ConsoleOut => Show a => HasIO io => a -> io ()

  Print a value to the console's standard output.

Totality: total
Visibility: export

cprintLn : ConsoleOut => Show a => HasIO io => a -> io ()

  Print a value plus trailing lne break
  to the console's standard output.

Totality: total
Visibility: export

cputErr : ConsoleOut => HasIO io => String -> io ()

  Put a string to the console's error output.

Totality: total
Visibility: export

cputErrLn : ConsoleOut => HasIO io => String -> io ()

  Put a string plus trailing line break
  to the console's error output.

Totality: total
Visibility: export

cprintErr : ConsoleOut => Show a => HasIO io => a -> io ()

  Print a value to the console's error output.

Totality: total
Visibility: export

cprintErrLn : ConsoleOut => Show a => HasIO io => a -> io ()

  Print a value plus trailing lne break
  to the console's error output.

Totality: total
Visibility: export

record ConsoleIn : Type

  Record representing a console with standard input.

Totality: total
Visibility: public export
Constructor: 

MkConsoleIn : IO Char -> IO String -> ConsoleIn

Projections:

.getChar_ : ConsoleIn -> IO Char

.getLine_ : ConsoleIn -> IO String

Hint: 

Console -> ConsoleIn

.getChar_ : ConsoleIn -> IO Char

Totality: total
Visibility: public export

getChar_ : ConsoleIn -> IO Char

Totality: total
Visibility: public export

.getLine_ : ConsoleIn -> IO String

Totality: total
Visibility: public export

getLine_ : ConsoleIn -> IO String

Totality: total
Visibility: public export

stdIn : ConsoleIn

  The default console, reading from standard input.

Totality: total
Visibility: export

cgetLine : ConsoleIn => HasIO io => io String

  Read a line from the console's standard input.

Totality: total
Visibility: export

cgetChar : ConsoleIn => HasIO io => io Char

  Read a single character from the console's standard input.

Totality: total
Visibility: export

record Console : Type

Totality: total
Visibility: public export
Constructor: 

MkConsole : ConsoleIn -> ConsoleOut -> Console

Projections:

.cin : Console -> ConsoleIn

.out : Console -> ConsoleOut

Hints:

Console -> ConsoleIn

Console -> ConsoleOut

.cin : Console -> ConsoleIn

Totality: total
Visibility: public export

cin : Console -> ConsoleIn

Totality: total
Visibility: public export

.out : Console -> ConsoleOut

Totality: total
Visibility: public export

out : Console -> ConsoleOut

Totality: total
Visibility: public export

stdIO : Console

Totality: total
Visibility: export

consoleOut : Console -> ConsoleOut

Totality: total
Visibility: export

consoleIn : Console -> ConsoleIn

Totality: total
Visibility: export