From 0859bb006ed2356ca6f5f47306e557260644effd Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 8 Oct 2024 18:12:31 +0900
Subject: [PATCH] =?UTF-8?q?`option`=20=E3=81=AE=E3=83=87=E3=83=95=E3=82=A9?=
 =?UTF-8?q?=E3=83=AB=E3=83=88=E5=80=A4=E3=82=92=E5=8F=96=E5=BE=97=E3=81=99?=
 =?UTF-8?q?=E3=82=8B=E9=96=A2=E6=95=B0=20Fixes=20#962?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Reference/Option/AutoImplicit.lean        | 33 +++++++++++++++----
 1 file changed, 27 insertions(+), 6 deletions(-)

diff --git a/LeanByExample/Reference/Option/AutoImplicit.lean b/LeanByExample/Reference/Option/AutoImplicit.lean
index 9727e060..d8530fc5 100644
--- a/LeanByExample/Reference/Option/AutoImplicit.lean
+++ b/LeanByExample/Reference/Option/AutoImplicit.lean
@@ -2,13 +2,8 @@
 `autoImplicit` オプションは、自動束縛暗黙引数(auto bound implicit arguments)という機能を制御します。
 
 有効にすると、宣言が省略された引数が1文字であるとき、それを暗黙引数として自動的に追加します。
-
-```admonish error title="非推奨"
-この機能には以下の問題点が指摘されており使用は推奨されません。
-* タイポを見過ごしやすくなってしまう
-* 自動束縛の結果どのような型になるか指定できないため、意図しない型に束縛されてバグを引き起こす可能性がある
-```
 -/
+import Lean --#
 set_option relaxedAutoImplicit false --#
 
 -- `autoImplicit` が無効の時
@@ -55,3 +50,29 @@ def nonempty₃ : List ℱ → Bool
     | _ :: _ => true
 
 end autoImpl
+
+/- ## 問題点
+
+```admonish error title="非推奨"
+この機能には以下の問題点が指摘されており使用は推奨されません。
+* タイポを見過ごしやすくなってしまう
+* 自動束縛の結果どのような型になるか指定できないため、意図しない型に束縛されてバグを引き起こす可能性がある
+```
+
+デフォルトではこのオプションは有効になっているため、`lakefile` の設定で無効にすることをお勧めします。
+-/
+
+open Lean Elab Command
+
+/-- オプションのデフォルト値を取得する関数 -/
+def getDefaultValue (opt : Name) : CommandElabM Unit := do
+  let decls ← getOptionDecls
+  match decls.find? opt with
+  | some decl =>
+    logInfo m!"default value of {opt} is {decl.defValue}"
+  | none =>
+    logInfo m!"{opt} is unknown"
+
+/-- info: default value of autoImplicit is true -/
+#guard_msgs in
+  #eval getDefaultValue `autoImplicit