コードの説明文のミスを修正

lean-ja · Jan 9, 2025 · 003b772 · 003b772
1 parent f9aa505
commit 003b772
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LeanByExample/Option/RelaxedAutoImplicit.lean b/LeanByExample/Option/RelaxedAutoImplicit.lean
@@ -22,7 +22,7 @@ section
   -- `relaxedAutoImplicit` が有効の時
   set_option relaxedAutoImplicit true
 
-  -- 二文字の識別子も自動束縛の対象になるのでエラーになる
+  -- 二文字の識別子も自動束縛の対象になるのでエラーにならない
   def nonempty₂ : List AB → Bool
     | [] => false
     | _ :: _ => true