From a8b80fa62e388f36d7dc2d4d106380fbb6d5ee5e Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 17 Nov 2024 22:06:36 +0900
Subject: [PATCH] =?UTF-8?q?#lint=20=E3=82=B3=E3=83=9E=E3=83=B3=E3=83=89?=
 =?UTF-8?q?=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B=20Fixes=20#1132?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Diagnostic/Lint.lean | 28 ++++++++++++++++++++
 booksrc/SUMMARY.md                           |  1 +
 2 files changed, 29 insertions(+)
 create mode 100644 LeanByExample/Reference/Diagnostic/Lint.lean

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)