Merge pull request #590 from lean-ja/Seasawher/issue587

Seasawher/issue587

Examples/Command/Declarative/Abbrev.lean

@@ -16,7 +16,7 @@ error: failed to synthesize
 numerals are polymorphic in Lean, but the numeral `42` cannot be used in a context where the expected type is
   NaturalNumber
 due to the absence of the instance above
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #check (42 : NaturalNumber)
 

Examples/Command/Declarative/Class.lean

@@ -57,8 +57,7 @@ def instMonoid'Nat : Monoid' Nat where
 
 /- このとき構造体 `Monoid'` のフィールド `Monoid'.e` は、「`Monoid'` の項に対して `α` の要素を返す」関数なので、次のような型を持ちます。-/
 
-/-- info: Class.Monoid'.e {α : Type} (self : Monoid' α) : α -/
-#guard_msgs in #check Monoid'.e
+#check (Monoid'.e : {α : Type} → (self : Monoid' α) → α)
 
 /- `self : Monoid' α` が暗黙の引数ではなく明示的な引数なので、型クラスのように書くことはできません。-/
 
@@ -72,8 +71,7 @@ def instMonoid'Nat : Monoid' Nat where
 
 ここで(本物の)型クラスにおける単位元関数 `e` の型を調べてみると、`self : Monoid' α` が角括弧 `[ .. ]` で囲われていることがわかります。-/
 
-/-- info: Class.Monoid.e {α : Type} [self : Monoid α] : α -/
-#guard_msgs in #check Monoid.e
+#check (Monoid.e : {α : Type} → [self : Monoid α] → α)
 
 /- これは**インスタンス暗黙引数**と呼ばれるもので、この場合 Lean に対して `Monoid' α` 型の項を自動的に合成するよう指示することを意味します。また、型クラスのインスタンス暗黙引数を自動的に合成する手続きのことを、**型クラス解決**と呼びます。-/
 
@@ -178,6 +176,7 @@ instance : HasCardinal Bool := by
 inductive Ordinal : Type where
   | nat (n : Nat) : Ordinal
   | omega : Ordinal
+deriving DecidableEq
 
 def Ordinal.toString : Ordinal → String
   | Ordinal.nat n => ToString.toString n
@@ -195,7 +194,6 @@ def HasCardinal.card (X : Type) [h : HasCardinal X] : Ordinal :=
 export HasCardinal (card)
 
 -- Bool の濃度が計算できた
-/-- info: 2 -/
-#guard_msgs in #eval card Bool
+#guard card Bool = Ordinal.nat 2
 
 end Class --#

Examples/Command/Declarative/Infix.lean

@@ -59,6 +59,6 @@ elab "#expand_command " t:command : command => do
 
 /-- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => lxor lhs✝ rhs✝ -/
 #guard_msgs in
-#expand_command infix:50 " LXOR " => lxor
+  #expand_command infix:50 " LXOR " => lxor
 
 end Infix --#

Examples/Command/Declarative/Local.lean

@@ -65,7 +65,7 @@ error: <input>:1:6: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si
 'notation', 'postfix', 'prefix', 'simproc', 'syntax' or 'unif_hint'
 -/
 #guard_msgs in
-run_meta checkParse `command "local def"
+  run_meta checkParse `command "local def"
 
 /-
 数が多いためすべての例を挙げることはしませんが、いくつか紹介します。たとえば `instance` の場合、`local` を付けて登録したインスタンスがその `section` の内部限定になります。

Examples/Command/Declarative/Macro.lean

@@ -15,7 +15,8 @@ def checkParse (cat : Name) (s : String) : MetaM Unit := do
 
 -- 最初は `#greet` が未定義なので、合法的なLeanのコマンドとして認識されない
 /-- error: <input>:1:0: expected command -/
-#guard_msgs in run_meta checkParse `command "#greet"
+#guard_msgs in
+  run_meta checkParse `command "#greet"
 
 -- `#greet` コマンドを定義する
 scoped macro "#greet " : command => `(#eval "Hello World!")

Examples/Command/Declarative/Notation.lean

@@ -130,19 +130,6 @@ set_option pp.mvars false
 
 -- 等号（優先順位 50）より優先順位が低いという問題でエラーになる
 -- 上では60で定義しているのに、なぜ？
-/--
-warning: application type mismatch
-  Sum true
-argument
-  true
-has type
-  Bool : Type
-but is expected to have type
-  Type _ : Type (_ + 1)
----
-info: sorryAx (Type u_1) true ⊕ sorryAx (Type u_2) true : Type (max u_1 u_2)
--/
-#guard_msgs in
 #check_failure true ⊕ true = false
 
 -- 括弧を付けるとエラーにならない

Examples/Command/Declarative/Opaque.lean

@@ -70,7 +70,7 @@ structure Something where
 /--
 error: failed to synthesize
   Inhabited Something
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in opaque something : Something
 

Examples/Command/Declarative/Partial.lean

@@ -15,12 +15,12 @@ namespace WithoutPartial --#
 error: fail to show termination for
   WithoutPartial.M
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter n:
   failed to eliminate recursive application
     M (n + 11)
 
+
 failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
@@ -30,12 +30,12 @@ h✝ : ¬n > 100
 ⊢ n + 11 < n
 -/
 #guard_msgs in
-/-- McCarthy の 91 関数 -/
-def M (n : Nat) : Nat :=
-  if n > 100 then
-    n - 10
-  else
-    M (M (n + 11))
+  /-- McCarthy の 91 関数 -/
+  def M (n : Nat) : Nat :=
+    if n > 100 then
+      n - 10
+    else
+      M (M (n + 11))
 
 end WithoutPartial --#
 namespace Partial --#

Examples/Command/Declarative/Scoped.lean

@@ -62,7 +62,7 @@ error: <input>:1:7: expected 'binder_predicate', 'builtin_dsimproc', 'builtin_si
 'syntax' or 'unif_hint'
 -/
 #guard_msgs in
-run_meta checkParse `command "scoped def"
+  run_meta checkParse `command "scoped def"
 
 /- ## open scoped
 `open scoped` コマンドを利用すると、特定の名前空間にある `scoped` が付けられた名前だけを有効にすることができます。単に [`open`](./Open.md) コマンドを利用するとその名前空間にあるすべての名前が有効になります。

Examples/Command/Declarative/TerminationBy.lean

@@ -7,12 +7,12 @@ namespace TerminationBy --#
 error: fail to show termination for
   TerminationBy.M
 with errors
-structural recursion cannot be used:
-
-argument #1 cannot be used for structural recursion
+failed to infer structural recursion:
+Cannot use parameter n:
   failed to eliminate recursive application
     M (n + 11)
 
+
 failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation

Examples/Command/Diagnostic/Eval.lean

@@ -26,10 +26,28 @@ def main : IO Unit :=
 式の評価を行うコマンドであるため、型や関数など、評価のしようがないものを与えるとエラーになります。-/
 
 -- 型は評価できない
-#guard_msgs (drop error) in #eval Nat
+/--
+error: expression
+  ℕ
+has type
+  Type
+but instance
+  Lean.MetaEval Type
+failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
+-/
+#guard_msgs in #eval Nat
 
 -- 関数そのものも評価できない
-#guard_msgs (drop error) in #eval (fun x => x + 1)
+/--
+error: expression
+  fun x => x + 1
+has type
+  ℕ → ℕ
+but instance
+  Lean.MetaEval (ℕ → ℕ)
+failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
+-/
+#guard_msgs in #eval (fun x => x + 1)
 
 /- 一般に、[`Repr`](../../Term/TypeClass/Repr.md) や [`ToString`](../../Term/TypeClass/ToString.md) のインスタンスでないような型の項は `#eval` に渡すことができません。-/
 

Examples/Command/Diagnostic/GuardMsgs.lean

@@ -6,17 +6,16 @@
 import Mathlib.Algebra.Group.Defs -- 逆数を使うために必要 --#
 
 /-- info: 2 -/
-#guard_msgs in
-#eval 2
+#guard_msgs in #eval 2
 
 /--
 error: failed to synthesize
   HAdd ℕ String String
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #eval (2 + "hello" : String)
 
-/-! ## 空白の扱い
+/- ## 空白の違いを無視させるには
 `#guard_msgs` コマンドは空白の数に敏感で、空白の長さによって通ったり通らなかったりします。しかし、`whitespace` という引数に `lax` を指定することにより、この空白に関する制限は緩めることができます。
 -/
 
@@ -26,7 +25,7 @@ variable (α : Type)
 /--
 error: failed to synthesize
   Inv α
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #check (_ : α)⁻¹
 
@@ -35,6 +34,6 @@ use `set_option diagnostics true` to get diagnostic information
 error:
   failed to synthesize
     Inv α
-  use `set_option diagnostics true` to get diagnostic information
+  Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in #check (_ : α)⁻¹

Examples/Command/Diagnostic/Print.lean

@@ -56,9 +56,9 @@ but is expected to have type
   TSyntax [`ident, `str] : Type
 -/
 #guard_msgs(error) in
-#eval show Lean.Elab.Term.TermElabM Unit from do
-  let a ← `(Nat.succ Nat.zero)
-  let _b ← `(#print $a)
+  #eval! show Lean.Elab.Term.TermElabM Unit from do
+    let a ← `(Nat.succ Nat.zero)
+    let _b ← `(#print $a)
 
 /- 上のコード例は、これを検証するものです。エラーメッセージにあるように `#print` は `ident` または `str` を期待しており、これはそれぞれ単一の識別子と文字列リテラルを意味します。`Nat.succ Nat.zero` は `term` つまり項なのでエラーになります。
 

Examples/Command/Diagnostic/Synth.lean

@@ -20,7 +20,7 @@ variable (α : Type)
 /--
 error: failed to synthesize
   Inv α
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #check (_ : α)⁻¹
 
@@ -35,13 +35,17 @@ use `set_option diagnostics true` to get diagnostic information
 
 /-! 自然数 `ℕ` に対しては逆数が定義されていないと予想されますが、実際 `Inv` のインスタンスになっていません。-/
 
+-- エラーになってしまう
 /--
 error: failed to synthesize
   Inv ℕ
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #synth Inv Nat
 
+-- Inv のインスタンスになっていない
+#check_failure (inferInstance : Inv Nat)
+
 /-! 自分で無理やり `ℕ` を `Inv` のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に `1` になる定数関数としてみましょう。-/
 
 instance : Inv Nat := ⟨fun _ => 1⟩

Examples/Command/Diagnostic/Whnf.lean

@@ -99,11 +99,10 @@ info: {
             ⟨fun x =>
               (Many.rec ⟨fun x => x, PUnit.unit⟩
                     (fun a a_2 a_ih =>
-                      ⟨fun x => Many.more a fun x_1 => (a_ih PUnit.unit).1 x,
-                        ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+                      ⟨fun x => Many.more a fun x_1 => (a_ih PUnit.unit).1 x, fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
                     (x a)).1
                 ((a_ih PUnit.unit).1 x),
-              ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+              fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
           x).1
       fun x => Many.more (f x) fun x => Many.none,
   mapConst := fun {α β} x x_1 =>
@@ -112,11 +111,10 @@ info: {
             ⟨fun x =>
               (Many.rec ⟨fun x => x, PUnit.unit⟩
                     (fun a a_2 a_ih =>
-                      ⟨fun x => Many.more a fun x_2 => (a_ih PUnit.unit).1 x,
-                        ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+                      ⟨fun x => Many.more a fun x_2 => (a_ih PUnit.unit).1 x, fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
                     (x a)).1
                 ((a_ih PUnit.unit).1 x),
-              ⟨⟨fun a => (a_ih a).1, fun a => (a_ih a).2⟩, PUnit.unit⟩⟩)
+              fun a => (a_ih a).1, fun a => (a_ih a).2⟩)
           x_1).1
       fun x_2 => Many.more x fun x => Many.none }
 -/

Examples/Tactic/AcRfl.lean

@@ -87,16 +87,11 @@ local に宣言したので、このセクション内限定 -/
 local instance : Std.Commutative (α := Color) (· + ·) where
   comm := Color.add_comm
 
-/--
-error: tactic 'rfl' failed, equality lhs
-  a + b
-is not definitionally equal to rhs
-  b + a
-a b : Color
-⊢ a + b = b + a
--/
-#guard_msgs in example (a b : Color) : a + b = b + a := by
-  ac_rfl
+example (a b : Color) : a + b = b + a := by
+  -- ac_rfl がエラーになってしまう
+  fail_if_success ac_rfl
+
+  ext <;> apply Nat.add_comm
 
 end
 /- ## 結合法則と ac_rfl
@@ -110,8 +105,13 @@ protected theorem add_assoc (a b c : Color) : a + b + c = a + (b + c) := by
 
 -- エラーになっているので、
 -- Commutative のインスタンスはないことが確認できる
-#guard_msgs (drop error) in
-#synth Std.Commutative (α := Color) (· + ·)
+/--
+error: failed to synthesize
+  Std.Commutative fun x x_1 => x + x_1
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+  #synth Std.Commutative (α := Color) (· + ·)
 
 /-- `add_comm` を `Std.Associative` に登録する。
 local にしたのでセクション内でのみ有効 -/

Examples/Tactic/Dsimp.lean

@@ -162,4 +162,4 @@ run_meta checkParse `tactic "unfold Inter.inter"
 -- 識別子でないものを渡すとパースできない
 /-- error: <input>:1:7: expected identifier -/
 #guard_msgs in
-run_meta checkParse `tactic "unfold (· ∩ ·)"
+  run_meta checkParse `tactic "unfold (· ∩ ·)"

Examples/Tactic/Ext.lean

@@ -45,10 +45,10 @@ attribute [ext] Point
 
 -- 自動生成された定理
 -- 各フィールドの値が等しければ、2つの `Point` は等しいという主張
-#check (Point.ext : (x y : Point α) → x.x = y.x → x.y = y.y → x = y)
+#check (Point.ext : ∀{x y : Point α}, x.x = y.x → x.y = y.y → x = y)
 
 -- 自動生成された定理その２
 -- 2つの `Point` の点が等しいことは、各フィールドの値が等しいことと同値
-#check (Point.ext_iff : (x y : Point α) → x = y ↔ x.x = y.x ∧ x.y = y.y)
+#check (Point.ext_iff : ∀{x y : Point α}, x = y ↔ x.x = y.x ∧ x.y = y.y)
 
 end Ext --#

Examples/Tactic/NativeDecide.lean

@@ -2,7 +2,7 @@
 # native_decide
 `native_decide` は、式を評価したときに判ることを示すことができます。
 
-たとえば、Lean では再帰関数 `f` を定義したらそれが停止することの証明を求められますが、それを `sorry` で回避したとしましょう。このとき `f` の具体的な値を `#eval` で評価することは依然として可能ですが、その値をとることを `rfl` で証明することはできなくなります。
+たとえば、Lean では再帰関数 `f` を定義したらそれが停止することの証明を求められますが、それを `sorry` で回避したとしましょう。このとき `f` の具体的な値を評価することは `#eval!` を使えば可能ですが、その値をとることを `rfl` で証明することはできなくなります。
 
 しかし、`native_decide` を使うと証明が可能です。
 -/
@@ -18,8 +18,8 @@ def gcd (m n : Nat) : Nat :=
   -- 停止性を証明しない
   decreasing_by sorry
 
--- eval はできる
-#eval gcd 42998431 120019
+-- 値を評価することはできる
+#eval! gcd 42998431 120019
 
 -- `rfl` では証明できない
 -- これは停止性を証明していないため

Examples/Term/TypeClass/ToString.lean

@@ -15,7 +15,7 @@ def origin : Point Int := ⟨0, 0⟩
 /--
 error: failed to synthesize
   ToString (Point Int)
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (error) in #check s!"{origin}"
 
@@ -57,8 +57,10 @@ def david := Person.mk "David" 42
 /--
 error: failed to synthesize
   ToString Person
-use `set_option diagnostics true` to get diagnostic information
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+info: toString "" ++ sorryAx String true ++ toString "" : String
 -/
-#guard_msgs (error) in #check s!"{david}"
+#guard_msgs in #check s!"{david}"
 
 end ToString --#