diff --git a/LeanByExample/Reference/Diagnostic/Lint.lean b/LeanByExample/Reference/Diagnostic/Lint.lean new file mode 100644 index 0000000..03d8f1e --- /dev/null +++ b/LeanByExample/Reference/Diagnostic/Lint.lean @@ -0,0 +1,28 @@ +/- # \#lint + +`#lint` コマンドは、リンタ(よくない書き方をされたコードを指摘してくれるツール)を実行します。 + +たとえば、以下は「ドキュメントコメントのない定理に対して警告するリンタ」を実行する例です。 +-/ +import Batteries.Tactic.Lint + +-- ドキュメントコメントのない定理 +theorem hoge : True := by trivial + +-- エラーにならない +/-- +info: -- Found 0 errors in 1 declarations +(plus 0 automatically generated ones) in the current file with 1 linters + +-- All linting checks passed! +-/ +#guard_msgs (whitespace := lax) in + -- 定義にドキュメントコメントがあるか確認するリンタ + -- 定理は対象外なのでスルーされる + #lint only docBlame + +-- 技術的な理由で `#lint` の出力は省略しているが、 +-- エラーになっている +#guard_msgs (drop error) in + -- ドキュメントコメントのない定理に対して警告するリンタを実行している + #lint only docBlameThm diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index c6bc60c..f16391c 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -17,6 +17,7 @@ - [#guard: Bool 値のテスト](./Reference/Diagnostic/Guard.md) - [#help: ドキュメントを見る](./Reference/Diagnostic/Help.md) - [#instances: インスタンスを列挙](./Reference/Diagnostic/Instances.md) + - [#lint: リンタ実行](./Reference/Diagnostic/Lint.md) - [#print: 中身を見る](./Reference/Diagnostic/Print.md) - [#reduce: 式を簡約する](./Reference/Diagnostic/Reduce.md) - [#synth: 型クラスの検査](./Reference/Diagnostic/Synth.md)