relaxedAutoImplicit オプションを紹介する

LeanByExample/Reference/Option/AutoImplicit.lean

@@ -1,5 +1,5 @@
 /- # autoImplicit
-`autoImplicit` オプションは、自動束縛暗黙引数(auto bound implicit arguments)という機能を制御します。
+`autoImplicit` オプションは、自動束縛暗黙引数(auto bound implicit arguments)という機能を制御します。類似オプションとして [`relaxedAutoImplicit`](./RelaxedAutoImplicit.md) があります。
 
 有効にすると、宣言が省略された引数が1文字であるとき、それを暗黙引数として自動的に追加します。
 -/

LeanByExample/Reference/Option/RelaxedAutoImplicit.lean

@@ -0,0 +1,55 @@
+/- # relaxedAutoImplicit
+
+`relaxedAutoImplicit` オプションは、[`autoImplicit`](./AutoImplicit.md) オプションの派生オプションであり、自動束縛の対象を広げます。
+-/
+import Lean --#
+-- `autoImplicit` は有効にしておく
+set_option autoImplicit true
+
+section
+  -- `relaxedAutoImplicit` が無効の時
+  set_option relaxedAutoImplicit false
+
+  -- 二文字の識別子は自動束縛の対象にならないのでエラーになる
+  /-- error: unknown identifier 'AB' -/
+  #guard_msgs in
+    def nonempty₁ : List AB → Bool
+      | [] => false
+      | _ :: _ => true
+end
+
+section
+  -- `relaxedAutoImplicit` が有効の時
+  set_option relaxedAutoImplicit true
+
+  -- 二文字の識別子も自動束縛の対象になるのでエラーになる
+  def nonempty₂ : List AB → Bool
+    | [] => false
+    | _ :: _ => true
+end
+
+/- ## 問題点
+
+```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 relaxedAutoImplicit is true -/
+#guard_msgs in
+  #eval getDefaultValue `relaxedAutoImplicit

booksrc/SUMMARY.md

@@ -76,6 +76,7 @@
   - [autoImplicit: 自動束縛暗黙引数](./Reference/Option/AutoImplicit.md)
   - [flexible: 脆弱な証明を指摘するリンタ](./Reference/Option/Flexible.md)
   - [hygiene: マクロ衛生](./Reference/Option/Hygiene.md)
+  - [relaxedAutoImplicit: 更にautoImplicit](./Reference/Option/RelaxedAutoImplicit.md)
 
 - [型クラス](./Reference/TypeClass/README.md)
   - [Coe: 型強制](./Reference/TypeClass/Coe.md)