21.3. 控制台输出🔗

Lean 包括用于写入标准输出和标准错误的便捷函数。全部都使用 ToString 实例，并且名称以 -ln 结尾的变体在输出后添加换行符。这些便捷函数只公开了使用标准 I/O 流时可用功能的一部分。特别是，要从标准输入读取一行，请使用 IO.getStdin 和 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

该程序演示了控制台 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."

它将以下内容输出到标准输出：

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

以及标准错误的以下内容：

stderrPlease report any errors so they can be corrected.