Merge pull request #218 from lean-ja/Seasawher/issue205

section/autoimplicit の例がfileplayでは正しく動作しない
lean-ja · Jun 10, 2024 · f312ae1 · f312ae1
2 parents 6e09d49 + 113bd03
commit f312ae1
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Examples/Syntax/Section.lean b/Examples/Syntax/Section.lean
@@ -13,6 +13,7 @@
 
 次は `variable` のスコープを区切る例です．
 -/
+set_option autoImplicit false --#
 
 section
   variable (a : Type)