From 8bb5c5d7913200063355b465298e6db12e3c1c3e Mon Sep 17 00:00:00 2001 From: Seasawher Date: Wed, 13 Nov 2024 03:39:59 +0900 Subject: [PATCH] =?UTF-8?q?=E3=82=AA=E3=83=97=E3=82=B7=E3=83=A7=E3=83=B3?= =?UTF-8?q?=E3=81=AE=E6=9C=89=E5=8A=B9=E7=AF=84=E5=9B=B2=E3=81=AE=E5=95=8F?= =?UTF-8?q?=E9=A1=8C=E3=82=92=E4=BF=AE=E6=AD=A3=E3=81=99=E3=82=8B?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Option/Flexible.lean | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/LeanByExample/Reference/Option/Flexible.lean b/LeanByExample/Reference/Option/Flexible.lean index 428a922..26e25c0 100644 --- 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