From 113bd03ee45237ed21335d6ee747f689693906cf Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 10 Jun 2024 22:24:14 +0900
Subject: [PATCH] =?UTF-8?q?section/autoimplicit=20=E3=81=AE=E4=BE=8B?=
 =?UTF-8?q?=E3=81=8Cfileplay=E3=81=A7=E3=81=AF=E6=AD=A3=E3=81=97=E3=81=8F?=
 =?UTF-8?q?=E5=8B=95=E4=BD=9C=E3=81=97=E3=81=AA=E3=81=84=20Fixes=20#205?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Syntax/Section.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Examples/Syntax/Section.lean b/Examples/Syntax/Section.lean
index eeb466ae..17e6629d 100644
--- a/Examples/Syntax/Section.lean
+++ b/Examples/Syntax/Section.lean
@@ -13,6 +13,7 @@
 
 次は `variable` のスコープを区切る例です．
 -/
+set_option autoImplicit false --#
 
 section
   variable (a : Type)