9.3. コンソール出力（Console Output）

Lean は標準出力と標準エラーに書き出すための便利な関数を有しています。それらは全て ToString インスタンスを使用し、そのうち名前が -ln で終わるものは出力の後に改行を追加します。これらの便利な関数は標準 I/O ストリームを使用する機能の一部しか公開していません。特に、標準入力から行を読むには、 IO.getStdin と 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

表示

このプログラムはコンソール I/O のための4つの便利な関数をすべて示しています。

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

これは以下を標準出力に書き出します：

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

また以下を標準エラーに書き出します：

stderrPlease report any errors so they can be corrected.