21.3. 控制台输出🔗

Lean 提供了向标准输出和标准错误写入内容的便捷函数。这些函数都使用 ToString 实例；名称以 -ln 结尾的变体会在输出后添加换行符。这些便捷函数只暴露了标准 I/O 流所提供的一部分功能。特别是，要从标准输入读取一行，应组合使用 IO.getStdin 与 IO.FS.Stream.getLine。

定义

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

使用 ToString α 实例将 s 转换为字符串，并将其打印到当前标准输出（由 IO.getStdout 决定）。

定义

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

使用 ToString α 实例将 s 转换为字符串，并在其后附加换行符，将其打印到当前标准输出（由 IO.getStdout 决定）。

定义

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

使用 ToString α 实例将 s 转换为字符串，并将其打印到当前标准错误（由 IO.getStderr 决定）。

定义

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

使用 ToString α 实例将 s 转换为字符串，并在其后附加换行符，将其打印到当前标准错误（由 IO.getStderr 决定）。

打印

该程序演示了全部四个控制台 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.