15.3. Console Output

Lean includes convenience functions for writing to standard output and standard error. All make use of ToString instances, and the varieties whose names end in -ln add a newline after the output. These convenience functions only expose a part of the functionality available using the standard I/O streams. In particular, to read a line from standard input, use a combination of IO.getStdin and IO.FS.Stream.getLine.

def

IO.print.{u_1} {α : Type u_1} [ToString α] (s : α) : IO Unit
IO.print.{u_1} {α : Type u_1} [ToString α]
  (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it to the current standard output (as determined by IO.getStdout).

def

IO.println.{u_1} {α : Type u_1} [ToString α] (s : α) : IO Unit
IO.println.{u_1} {α : Type u_1}
  [ToString α] (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it with a trailing newline to the current standard output (as determined by IO.getStdout).

def

IO.eprint.{u_1} {α : Type u_1} [ToString α] (s : α) : IO Unit
IO.eprint.{u_1} {α : Type u_1}
  [ToString α] (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it to the current standard error (as determined by IO.getStderr).

def

IO.eprintln.{u_1} {α : Type u_1} [ToString α] (s : α) : IO Unit
IO.eprintln.{u_1} {α : Type u_1}
  [ToString α] (s : α) : IO Unit

Converts s to a string using its ToString α instance, and prints it with a trailing newline to the current standard error (as determined by IO.getStderr).

Printing

This program demonstrates all four convenience functions for console I/O.

def main : IO Unit := do
  IO.print "This is the "
  IO.print "Lean"
  IO.println " language reference."
  IO.println "Thank you for reading it!"
  IO.eprint "Please report any "
  IO.eprint "errors"
  IO.eprintln " so they can be corrected."

It outputs the following to the standard output:

stdoutThis is the Lean language reference.Thank you for reading it!

and the following to the standard error:

stderrPlease report any errors so they can be corrected.