オプションの有効範囲の問題を修正する

lean-ja · Nov 12, 2024 · 8bb5c5d · 8bb5c5d
1 parent 582ec41
commit 8bb5c5d
Showing 1 changed file with 1 addition and 5 deletions.
diff --git a/LeanByExample/Reference/Option/Flexible.lean b/LeanByExample/Reference/Option/Flexible.lean
@@ -55,17 +55,13 @@ end --#
 -/
 section --#
 
--- 技術的な理由で、一時的に flexible tactic リンタを無効にしている --#
-set_option linter.flexible false --#
+set_option linter.flexible true
 
 /--
 warning: 'simp' is a flexible tactic modifying '⊢'…
 note: this linter can be disabled with `set_option linter.flexible false`
 -/
 #guard_msgs (warning) in
-  -- 技術的な理由で、`#guard_msgs` のスコープ内でリンタを有効にしている
-  set_option linter.flexible true in
-
   example {n m : Nat} (h : n = m) : True ∧ (n = m) := by
     simp
     exact h