autoImplicit オプションを紹介する

Examples/Option/AutoImplicit.lean

@@ -0,0 +1,57 @@
+/- # autoImplicit
+`autoImplicit` オプションは、自動束縛暗黙引数(auto bound implicit arguments)という機能を制御します。
+
+有効にすると、宣言が省略された引数が1文字であるとき、それを暗黙引数として自動的に追加します。
+
+```admonish error title="非推奨"
+この機能には以下の問題点が指摘されており使用は推奨されません。
+* タイポを見過ごしやすくなってしまう
+* 自動束縛の結果どのような型になるか指定できないため、意図しない型に束縛されてバグを引き起こす可能性がある
+```
+-/
+set_option relaxedAutoImplicit false --#
+
+-- `autoImplicit` が無効の時
+set_option autoImplicit false in
+
+-- `nonempty` の定義には `α` という未定義の識別子が含まれるため、
+-- エラーになる
+/-- error: unknown identifier 'α' -/
+#guard_msgs in
+  def nonempty : List α → Bool
+    | [] => false
+    | _ :: _ => true
+
+-- `autoImplicit` が有効の時
+set_option autoImplicit true in
+
+-- `α` という未定義の識別子を含んでいてもエラーにならない。
+-- 勝手に暗黙引数として追加されている
+def head : List α → Option α
+  | [] => none
+  | x :: _ => some x
+
+/- 1文字の未束縛の識別子であればなんでも対象になるようです。 -/
+section autoImpl
+
+-- `autoImplicit` が有効の時
+set_option autoImplicit true
+
+-- ギリシャ文字ではなくて1文字の小文字でも暗黙引数として追加される
+def nonempty₂ : List a → Bool
+  | [] => false
+  | _ :: _ => true
+
+-- `ℱ` も暗黙引数になる
+def nonempty₃ : List ℱ → Bool
+  | [] => false
+  | _ :: _ => true
+
+-- ２文字の識別子は暗黙引数として追加されない
+/-- error: unknown identifier 'AB' -/
+#guard_msgs in
+  def nonempty₄ : List AB → Bool
+    | [] => false
+    | _ :: _ => true
+
+end autoImpl

src/SUMMARY.md

@@ -71,7 +71,8 @@
   - [simps: simp 補題の自動生成](./Attribute/Simps.md)
 
 - [オプション](./Option/README.md)
-  - [hygiene: マクロ衛生](./Option/Hygine.md)
+  - [autoImplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md)
+  - [hygiene: マクロ衛生](./Option/Hygiene.md)
 
 - [型クラス](./TypeClass/README.md)
   - [Coe: 型強制](./TypeClass/Coe.md)