warning が出ないようにする

Fixes #943

.vscode/lean.code-snippets

@@ -16,4 +16,20 @@
     ],
     "description": "doc string"
   },
+  "drop warning": {
+    "scope": "lean,lean4",
+    "prefix": "dropwarn",
+    "body": [
+      "#guard_msgs (drop warning) in --#",
+    ],
+    "description": "drop warning"
+  },
+  "unusedTactic linter disable": {
+    "scope": "lean,lean4",
+    "prefix": "unusedTactic",
+    "body": [
+      "set_option linter.unusedTactic false in --#",
+    ],
+    "description": "unusedTactic linter disable"
+  }
 }

Examples/Declarative/Class.lean

@@ -61,6 +61,7 @@ def instMonoid'Nat : Monoid' Nat where
 
 /- `self : Monoid' α` が暗黙の引数ではなく明示的な引数なので、型クラスのように書くことはできません。-/
 
+#guard_msgs (drop warning) in --#
 #check_failure (Monoid'.e : Nat)
 
 /- しかし、インスタンスを引数として渡せば、型クラスのように `Nat` の要素を取り出すことができます。-/

Examples/Declarative/DeclareSyntaxCat.lean

@@ -44,8 +44,11 @@ syntax "{" binder "|" term "}" : term
 
 -- 合法な構文として認識される
 -- 実装は与えていないのでエラーにはなる
+#guard_msgs (drop warning) in --#
 #check_failure { x | x = 0}
+#guard_msgs (drop warning) in --#
 #check_failure { x : Nat | x > 0 }
+#guard_msgs (drop warning) in --#
 #check_failure { x ∈ T | x = 0}
 
 /-- `{x : T | P x}` と `{x ∈ T | P x}` の形の式を `setOf` の式に変換する -/

Examples/Declarative/Export.lean

@@ -6,7 +6,7 @@
 
 * [`open`](./Open.md) と同様に、`nameᵢ` が `Some.Namespace` の接頭辞なしで現在の名前空間 `N` 上で見えるようになります。
 * 現在の名前空間 `N` の外部の名前空間から `N.nameᵢ` としてアクセスできるようになります。
- -/
+-/
 namespace N -- export コマンドが実行される名前空間
 
   inductive Sample : Type where
@@ -16,6 +16,7 @@ namespace N -- export コマンドが実行される名前空間
 
   -- foo は名前空間 Sample 上にあるので、
   -- 短い名前ではアクセスできない
+  #guard_msgs (drop warning) in --#
   #check_failure foo
   #check Sample.foo
 
@@ -29,6 +30,7 @@ end N
 
 -- 名前空間 `N` の外部からアクセスするには、
 -- 普通はフルネームが必要
+#guard_msgs (drop warning) in --#
 #check_failure N.bar
 #check N.Sample.bar
 

Examples/Declarative/Infix.lean

@@ -26,6 +26,7 @@ scoped infix:51 " strong " => Nat.add
 -- したがってエラーになる
 scoped infix:49 " weak " => Nat.add
 
+#guard_msgs (drop warning) in --#
 #check_failure 1 + 2 weak 3 = 6
 
 /- `infix` で定義される記法は左結合でも右結合でもなく、必ず括弧が必要です。-/

Examples/Declarative/Instance.lean

@@ -13,6 +13,7 @@ structure Point (α : Type) where
 def origin : Point Int := { x := 0, y := 0 }
 
 -- 数値のように足し算をすることはできない
+#guard_msgs (drop warning) in --#
 #check_failure (origin + origin)
 
 /-- 平面上の点の足し算ができるようにする -/
@@ -57,6 +58,7 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 #guard (2 : Even) = Even.succ Even.zero
 
 -- 奇数については OfNat の実装はない
+#guard_msgs (drop warning) in --#
 #check_failure (3 : Even)
 
 /- なお、インスタンス連鎖の回数には上限があります。-/
@@ -65,6 +67,7 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 #eval (254 : Even)
 
 -- 上限を超えてしまった
+#guard_msgs (drop warning) in --#
 #check_failure (256 : Even)
 
 /-
@@ -73,6 +76,7 @@ instance {n : Nat} [OfNat Even n] : OfNat Even (n + 2) where
 -/
 
 -- `List` 同士を足すことはできない
+#guard_msgs (drop warning) in --#
 #check_failure [1] + [2]
 
 -- インスタンスを宣言する
@@ -88,6 +92,7 @@ def instListAdd {α : Type} : Add (List α) where
 attribute [-instance] instListAdd
 
 -- リスト同士を足すことができなくなった
+#guard_msgs (drop warning) in --#
 #check_failure [1] + [2]
 
 end Instance --#

Examples/Declarative/Local.lean

@@ -11,10 +11,12 @@ section foo
 end foo
 
 -- section を抜けると使えなくなる
+#guard_msgs (drop warning) in --#
 #check_failure succ'
 
 section foo
   -- 同じ名前の section を再度開いても使えない
+  #guard_msgs (drop warning) in --#
   #check_failure succ'
 end foo
 
@@ -29,11 +31,13 @@ namespace hoge
 end hoge
 
 -- namespace の外では使用できない
+#guard_msgs (drop warning) in --#
 #check_failure succ' 2
 
 -- 再び同じ名前の namespace をオープンする
 namespace hoge
   -- 使用できない！
+  #guard_msgs (drop warning) in --#
   #check_failure succ'
 end hoge
 
@@ -85,6 +89,7 @@ section
 end
 
 -- section を抜けると使えなくなる
+#guard_msgs (drop warning) in --#
 #check_failure (0 : MyNat)
 
 /- ## 属性に対する local
@@ -110,4 +115,5 @@ section
 end
 
 -- section を抜けると simp 補題が利用できなくなる
+#guard_msgs (drop warning) in --#
 #check_failure (by simp : MyNat.add .zero .zero = .zero)

Examples/Declarative/MacroRules.lean

@@ -48,6 +48,7 @@ end Set
 syntax "{{" term,* "}}" : term
 
 -- `syntax` コマンドは記法の解釈方法を決めていないので、エラーになる
+#guard_msgs (drop warning) in --#
 #check_failure {{2, 3}}
 
 -- 集合の波括弧記法をどう解釈するかのルールを定める

Examples/Declarative/Namespace.lean

@@ -20,6 +20,7 @@ namespace Nat
 end Nat
 
 -- 名前空間の外に出ると、短い名前ではアクセスできない
+#guard_msgs (drop warning) in --#
 #check_failure isEven
 
 -- フルネームならアクセスできる

Examples/Declarative/Notation.lean

@@ -132,6 +132,7 @@ set_option pp.mvars false
 
 -- 等号（パース優先順位 50）より優先順位が低いという問題でエラーになる
 -- 上では60で定義しているのに、なぜ？
+#guard_msgs (drop warning) in --#
 #check_failure true ⊕ true = false
 
 -- 括弧を付けるとエラーにならない
@@ -158,6 +159,7 @@ local macro_rules | `($x ⊕ $y) => `(xor $x $y)
 #guard false ⊕ false = false
 
 -- 上書きされたので、 Sum の意味で ⊕ を使うことはできなくなった
+#guard_msgs (drop warning) in --#
 #check_failure Nat ⊕ Fin 2
 end --#
 

Examples/Declarative/Opaque.lean

@@ -99,6 +99,7 @@ opaque B : Type
 opaque C : Type
 
 -- 実装は与えないが C は Inhabited のインスタンスだと仮定
+#guard_msgs (drop warning) in --#
 instance : Inhabited C where
   default := sorry
 

Examples/Declarative/Open.lean

@@ -11,6 +11,7 @@ namespace Hoge
 end Hoge
 
 -- 名前空間の外からだと `foo` という短い名前が使えない
+#guard_msgs (drop warning) in --#
 #check_failure foo
 
 section
@@ -22,6 +23,7 @@ section
 end
 
 -- セクションが終わると再び短い名前は使えなくなる
+#guard_msgs (drop warning) in --#
 #check_failure foo
 
 /- ## 入れ子になった名前空間

Examples/Declarative/Private.lean

@@ -11,6 +11,7 @@ namespace Private --#
 #check Point.sub
 
 -- private とマークした定義にはアクセスできない
+#guard_msgs (drop warning) in --#
 #check_failure Point.private_sub
 
 /- なお `private` コマンドでセクションや名前空間にスコープを制限することはできません。-/

Examples/Declarative/ProofWanted.lean

@@ -12,10 +12,12 @@ variable (n : Nat)
 proof_wanted result : n + 0 = n
 
 -- sorry で同様のことができる
+#guard_msgs (drop warning) in --#
 theorem another_result : n + 0 = n := by sorry
 
 -- sorry で証明した定理は参照できるが
 #check another_result
 
 -- proof_wanted で宣言した定理は参照できない
+#guard_msgs (drop warning) in --#
 #check_failure result

Examples/Declarative/Protected.lean

@@ -16,6 +16,7 @@ namespace Point
   private def private_sub := Point.sub
 
   -- 名前空間の中にいても、短い名前ではアクセスできない
+  #guard_msgs (drop warning) in --#
   #check_failure sub
 
   -- フルネームならアクセスできる
@@ -26,6 +27,7 @@ end Point
 open Point
 
 -- 名前空間を開いていても、短い名前でアクセスできない
+#guard_msgs (drop warning) in --#
 #check_failure sub
 
 -- フルネームならアクセスできる
@@ -78,6 +80,7 @@ open BinTree
 
 -- 名前空間を開いているのに、
 -- コンストラクタに短い名前でアクセスできない
+#guard_msgs (drop warning) in --#
 #check_failure node
 #check BinTree.node
 
@@ -100,6 +103,7 @@ open Sample
 #check bar
 
 -- hoge には短い名前でアクセスできない
+#guard_msgs (drop warning) in --#
 #check_failure hoge
 
 end --#

Examples/Declarative/Scoped.lean

@@ -97,5 +97,6 @@ section
   #check (30 add' 12)
 
   -- greet は使えないまま
+  #guard_msgs (drop warning) in --#
   #check_failure greet
 end

Examples/Declarative/Section.lean

@@ -23,6 +23,7 @@ section
 end
 
 -- `section` の外に出ると無効になる
+#guard_msgs (drop warning) in --#
 #check_failure a
 
 /-
@@ -37,6 +38,7 @@ section
 end
 
 -- スコープが終わると無効になる
+#guard_msgs (drop warning) in --#
 #check_failure choice
 
 /- 次は `set_option` のスコープを区切る例です。 -/
@@ -86,8 +88,10 @@ section parent
   end child
 
   -- child セクションの外なので無効
+  #guard_msgs (drop warning) in --#
   #check_failure b
 end parent
 
 -- parent セクションの外なので無効
+#guard_msgs (drop warning) in --#
 #check_failure a

Examples/Declarative/Structure.lean

@@ -87,10 +87,16 @@ inductive Sample where
   | fst (foo bar : Nat) : Sample
   | snd (foo bar : String) : Sample
 
--- 「コンストラクタが一つしかない型でなければ使用できない」というエラーになる
-#check_failure (⟨"foo", "bar"⟩ : Sample)
+-- 「コンストラクタが一つしかない帰納型でなければ使用できない」というエラーになる
+/--
+warning: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor ⏎
+  Sample
+-/
+#guard_msgs in
+  #check_failure (⟨"foo", "bar"⟩ : Sample)
 
 -- コンストラクタを指定しても使用できない
+#guard_msgs (drop warning) in --#
 #check_failure (Sample.snd ⟨"foo", "bar"⟩ : Sample)
 
 /- ## 項を定義する様々な構文
@@ -146,12 +152,18 @@ inductive Point' (α : Type) : Type where
   | mk : (x : α) → (y : α) → Point' α
 
 -- フィールド記法が利用できない
+#guard_msgs (drop warning) in --#
 #check_failure Point'.x
 
 -- 無名コンストラクタは使用できる
 def origin' : Point Int := ⟨0, 0⟩
 
 -- 波括弧記法は使用できない
-#check_failure ({ x := 1, y := 2 } : Point' Int)
+/--
+warning: invalid {...} notation, structure type expected
+  Point' Int
+-/
+#guard_msgs in
+  #check_failure ({ x := 1, y := 2 } : Point' Int)
 
 end Structure --#

Examples/Diagnostic/CheckFailure.lean

@@ -3,10 +3,13 @@
 -/
 
 -- 自然数と文字列を足すことはできない
+#guard_msgs (drop warning) in --#
 #check_failure 1 + "hello"
 
 -- `1 = 2` を `rfl` で証明することはできない
+#guard_msgs (drop warning) in --#
 #check_failure (by rfl : 1 = 2)
 
 -- `1 + 4 = 5` は `contradiction` では示せない
+#guard_msgs (drop warning) in --#
 #check_failure (by contradiction : 1 + 4 = 5)

Examples/Diagnostic/Print.lean

@@ -34,6 +34,7 @@ example : ∀ (p : Prop), p ∨ ¬p := Classical.em
 
 /- また、`sorry` という命題を「証明したことにする」タクティクがありますが、これは `sorryAx` という万能な公理を導入していることが確認できます。-/
 
+#guard_msgs (drop warning) in --#
 theorem contra : False := by sorry
 
 /-- info: 'contra' depends on axioms: [sorryAx] -/

Examples/Diagnostic/Synth.lean

@@ -44,6 +44,7 @@ Additional diagnostic information may be available using the `set_option diagnos
 #guard_msgs in #synth Inv Nat
 
 -- Inv のインスタンスになっていない
+#guard_msgs (drop warning) in --#
 #check_failure (inferInstance : Inv Nat)
 
 /-! 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/

Examples/Option/Flexible.lean

@@ -0,0 +1,8 @@
+import Mathlib.Tactic
+
+set_option linter.flexible true
+
+example {n m : Nat} (h : n + 0 = m) : True ∧ (n = m) := by
+  constructor
+  all_goals
+    simp_all

Examples/Solution/CantorPairing.lean

@@ -108,7 +108,7 @@ theorem pair_unpair_eq_id (x : ℕ) : pair (unpair x) = x := by
       -- `sum (m + n) + m = x` を示せば良いことが分かる。
       suffices sum (m + n) + m = x from by
         -- sorry
-        simp [pair]
+        simp only [pair]
         rw [show m + 1 + (n - 1) = m + n from by omega]
         omega
         -- sorry

Examples/Tactic/ApplyQuestion.lean

@@ -22,7 +22,9 @@ example [Group G] [Group H] (f : G →* H) (a b : G) :
 `sorry` と同じように、清書した証明に残してはいけません。
 `sorry` と同じと言いましたが、実際 `apply?` は `sorryAx` を裏で使用します。
 -/
+set_option linter.unusedTactic false in --#
 
+#guard_msgs (drop warning) in --#
 theorem T (x y : Nat) (_: x ≤ y) : 8 ^ x ≤ 16 ^ y := by
   apply?