diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cbbefee5..a8ce1a2d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,7 +25,7 @@ jobs: - name: lean action uses: leanprover/lean-action@v1 with: - build-args: "--log-level=error" + build-args: "--fail-level=warning" # Lean の更新により Windows 環境でだけビルドが壊れる可能性もあるので、 # 念のために Windows 環境でもビルドを行う diff --git a/LeanByExample/Reference/Option/Flexible.lean b/LeanByExample/Reference/Option/Flexible.lean index 69a5980e..55647f78 100644 --- a/LeanByExample/Reference/Option/Flexible.lean +++ b/LeanByExample/Reference/Option/Flexible.lean @@ -55,14 +55,17 @@ end --# -/ section --# --- flexible tactic リンタを有効にする -set_option linter.flexible true +-- 技術的な理由で、一時的に flexible tactic リンタを無効にしている --# +set_option linter.flexible false --# /-- 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