warning を消す

lean-ja · Nov 8, 2024 · 1b097a2 · 1b097a2
1 parent 5ed46b5
commit 1b097a2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/LeanByExample/Reference/Tactic/Exact.lean b/LeanByExample/Reference/Tactic/Exact.lean
@@ -2,6 +2,7 @@
 
 ゴールが `P` で、ローカルコンテキストに `hP : P` があるときに、`exact hP` はゴールを閉じます。`hP` がゴールの証明になっていないときには、失敗してエラーになります。-/
 variable (P Q : Prop)
+set_option linter.unusedVariables false in --#
 
 example (hP : P) (hQ : Q) : P := by
   -- `hQ : Q` は `P` の証明ではないのでもちろん失敗する

diff --git a/LeanByExample/Reference/Tactic/Rw.lean b/LeanByExample/Reference/Tactic/Rw.lean
@@ -51,7 +51,7 @@ example (h : a = b) (hb : a + 3 = 0) : b + 3 = 0 := by
 
 また、ゴールとローカルコンテキストの仮定 `h` に対して同時に書き換えたいときは `⊢` 記号を使って `rw [hPQ] at h ⊢` のようにします。-/
 
-example (h : a + 0 = a) (h1 : b + (a + 0) = b + a) (h2 : a + (a + 0) = a)
+example (h : a + 0 = a) (_h1 : b + (a + 0) = b + a) (_h2 : a + (a + 0) = a)
     : a + 0 = 0 + a := by
   -- ローカルコンテキストとゴールのすべてに対して書き換えを行う
   rw [h] at *