宣言的コマンド、対話的コマンドという言葉について補足し、一般的な用語でないことを注意する

Seasawher · Seasawher · commit 1856946d8375 · 2025-01-01T17:52:29.000+09:00
diff --git a/LeanByExample/Declarative/README.lean b/LeanByExample/Declarative/README.lean
@@ -2,5 +2,7 @@
 
 トップレベルコマンドには `#` から始まるものとそうでないものがあり、そうでないものを本書では便宜的に「宣言的コマンド」と呼んでいます。これは、そうしたコマンドが定義を行ったり属性を付与したりと、Lean に何かを宣言するために使われることが多いためです。
 
-構文的には宣言的コマンドと対話的コマンドは同じ振る舞いをします。
+```admonish warning title="注意"
+宣言的コマンド(declarative command)という用語は Lean コミュニティでは通じると思いますが、一般的なものではありません。
+```
 -/
diff --git a/LeanByExample/Diagnostic/README.lean b/LeanByExample/Diagnostic/README.lean
@@ -1,5 +1,7 @@
 /- # 対話的コマンド
 トップレベルコマンドのうち、`#` から始まるものを本書では便宜的に「対話的コマンド」と呼んでいます。これは、そうしたコマンドの多くが「式を評価した値を調べる」「式の型を調べる」など Lean から情報を得るために使用されるからです。
 
-構文的には宣言的コマンドと対話的コマンドは同じ振る舞いをします。
+```admonish warning title="注意"
+対話的コマンド(diagnostic command)という用語は一般的なものではありません。Lean コミュニティで通じない可能性もあります。著者は diagnostic command という用語を [The Hitchhiker's Guide to Logical Verification](https://github.com/blanchette/interactive_theorem_proving_2024) から拝借しましたが、同じものが hash command と呼ばれているのを聞いたこともあります。決まった呼び方がないという印象です。
+```
 -/
