Skip to content
This repository was archived by the owner on Jan 5, 2025. It is now read-only.

Commit ae6da5f

Browse files
committed
翻訳開始
1 parent afbe1d7 commit ae6da5f

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

Manual/IO/Console.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,10 @@ set_option pp.rawOnError true
1818

1919
set_option linter.unusedVariables false
2020

21+
/-
2122
#doc (Manual) "Console Output" =>
23+
-/
24+
#doc (Manual) "コンソール出力(Console Output)" =>
2225

2326
Lean includes convenience functions for writing to {tech}[standard output] and {tech}[standard error].
2427
All make use of {lean}`ToString` instances, and the varieties whose names end in `-ln` add a newline after the output.

0 commit comments

Comments
 (0)