From c411ecdfe8b2752764537c8730166aeabb84acb9 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 5 Oct 2024 04:04:08 +0900 Subject: [PATCH 1/5] =?UTF-8?q?`autoimplicit`=20=E3=82=AA=E3=83=97?= =?UTF-8?q?=E3=82=B7=E3=83=A7=E3=83=B3=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99?= =?UTF-8?q?=E3=82=8B=20Fixes=20#939?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Option/Autoimplicit.lean | 57 +++++++++++++++++++++++++++++++ src/SUMMARY.md | 1 + 2 files changed, 58 insertions(+) create mode 100644 Examples/Option/Autoimplicit.lean diff --git a/Examples/Option/Autoimplicit.lean b/Examples/Option/Autoimplicit.lean new file mode 100644 index 00000000..84e987e2 --- /dev/null +++ b/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 diff --git a/src/SUMMARY.md b/src/SUMMARY.md index dbaa7670..c32945ee 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -71,6 +71,7 @@ - [simps: simp 補題の自動生成](./Attribute/Simps.md) - [オプション](./Option/README.md) + - [autoimplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md) - [hygiene: マクロ衛生](./Option/Hygine.md) - [型クラス](./TypeClass/README.md) From 87586fc88aca8c0f8ee88fb4d8b0de74043d2371 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 5 Oct 2024 04:19:17 +0900 Subject: [PATCH 2/5] =?UTF-8?q?=E5=A4=A7=E6=96=87=E5=AD=97=E3=81=A8?= =?UTF-8?q?=E5=B0=8F=E6=96=87=E5=AD=97=E3=81=AE=E5=A4=89=E6=8F=9B=E3=83=9F?= =?UTF-8?q?=E3=82=B9?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Option/Autoimplicit.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Examples/Option/Autoimplicit.lean b/Examples/Option/Autoimplicit.lean index 84e987e2..9727e060 100644 --- a/Examples/Option/Autoimplicit.lean +++ b/Examples/Option/Autoimplicit.lean @@ -1,5 +1,5 @@ -/- # autoimplicit -`autoimplicit` オプションは、自動束縛暗黙引数(auto bound implicit arguments)という機能を制御します。 +/- # autoImplicit +`autoImplicit` オプションは、自動束縛暗黙引数(auto bound implicit arguments)という機能を制御します。 有効にすると、宣言が省略された引数が1文字であるとき、それを暗黙引数として自動的に追加します。 @@ -11,7 +11,7 @@ -/ set_option relaxedAutoImplicit false --# --- `autoimplicit` が無効の時 +-- `autoImplicit` が無効の時 set_option autoImplicit false in -- `nonempty` の定義には `α` という未定義の識別子が含まれるため、 @@ -22,7 +22,7 @@ set_option autoImplicit false in | [] => false | _ :: _ => true --- `autoimplicit` が有効の時 +-- `autoImplicit` が有効の時 set_option autoImplicit true in -- `α` という未定義の識別子を含んでいてもエラーにならない。 @@ -34,7 +34,7 @@ def head : List α → Option α /- 1文字の未束縛の識別子であればなんでも対象になるようです。 -/ section autoImpl --- `autoimplicit` が有効の時 +-- `autoImplicit` が有効の時 set_option autoImplicit true -- ギリシャ文字ではなくて1文字の小文字でも暗黙引数として追加される From 6a8342058fc158e908d777d7c28bb105792a052d Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 5 Oct 2024 04:34:14 +0900 Subject: [PATCH 3/5] =?UTF-8?q?`autoImplicit`=20=E3=82=92=E3=83=91?= =?UTF-8?q?=E3=82=B9=E3=82=AB=E3=83=AB=E3=82=B1=E3=83=BC=E3=82=B9=E3=81=AB?= =?UTF-8?q?=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/SUMMARY.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index c32945ee..62408278 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -71,7 +71,7 @@ - [simps: simp 補題の自動生成](./Attribute/Simps.md) - [オプション](./Option/README.md) - - [autoimplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md) + - [autoImplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md) - [hygiene: マクロ衛生](./Option/Hygine.md) - [型クラス](./TypeClass/README.md) From c6d5e79f1db2ccc720960f38ae13e13992675692 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 5 Oct 2024 04:43:46 +0900 Subject: [PATCH 4/5] =?UTF-8?q?`hygiene`=20=E3=81=AE=E8=AA=A4=E5=AD=97?= =?UTF-8?q?=E3=82=92=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Option/{Hygine.lean => Hygiene.lean} | 0 src/SUMMARY.md | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename Examples/Option/{Hygine.lean => Hygiene.lean} (100%) diff --git a/Examples/Option/Hygine.lean b/Examples/Option/Hygiene.lean similarity index 100% rename from Examples/Option/Hygine.lean rename to Examples/Option/Hygiene.lean diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 62408278..d4c89743 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -72,7 +72,7 @@ - [オプション](./Option/README.md) - [autoImplicit: 自動束縛暗黙引数](./Option/AutoImplicit.md) - - [hygiene: マクロ衛生](./Option/Hygine.md) + - [hygiene: マクロ衛生](./Option/Hygiene.md) - [型クラス](./TypeClass/README.md) - [Coe: 型強制](./TypeClass/Coe.md) From 30385a5eda5616556260a5de49df9fb902d727dc Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 5 Oct 2024 04:48:12 +0900 Subject: [PATCH 5/5] =?UTF-8?q?=E3=82=BF=E3=82=A4=E3=83=9D=E3=81=97?= =?UTF-8?q?=E3=81=9F=E3=83=95=E3=82=A1=E3=82=A4=E3=83=AB=E3=82=92=E5=89=8A?= =?UTF-8?q?=E9=99=A4?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Option/{Autoimplicit.lean => AutoImplicit.lean} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename Examples/Option/{Autoimplicit.lean => AutoImplicit.lean} (100%) diff --git a/Examples/Option/Autoimplicit.lean b/Examples/Option/AutoImplicit.lean similarity index 100% rename from Examples/Option/Autoimplicit.lean rename to Examples/Option/AutoImplicit.lean