6.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

def

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

def

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

def

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

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.