test: adjust tests

Author: mhuisi

BatteriesTest/lemma_cmd.lean

@@ -3,7 +3,7 @@ import Batteries.Tactic.Lemma
 -- lemma disabled by default
 /--
 info: Try this:
-  theorem
+  [apply] theorem
 ---
 error: `lemma` is not supported by default, please use `theorem` instead.
 Use `set_option lang.lemmaCmd true` to enable the use of the `lemma` command in a file.
@@ -19,7 +19,7 @@ lemma test2 : 3 < 7 := by decide
 -- lemma disabled again
 /--
 info: Try this:
-  theorem
+  [apply] theorem
 ---
 error: `lemma` is not supported by default, please use `theorem` instead.
 Use `set_option lang.lemmaCmd true` to enable the use of the `lemma` command in a file.

BatteriesTest/show_term.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 
 /--
 info: Try this:
-  exact (n, 37)
+  [apply] exact (n, 37)
 -/
 #guard_msgs in example (n : Nat) : Nat × Nat := by
   show_term
@@ -16,15 +16,15 @@ info: Try this:
 
 /--
 info: Try this:
-  refine (?_, ?_)
+  [apply] refine (?_, ?_)
 -/
 #guard_msgs in example : Nat × Nat := by
   show_term constructor
   repeat exact 42
 
 /--
 info: Try this:
-  fun {X} => X
+  [apply] fun {X} => X
 -/
 #guard_msgs in example : {_a : Nat} → Nat :=
   show_term by

BatteriesTest/simp_trace.lean

@@ -7,13 +7,13 @@ set_option linter.missingDocs false
 
 /--
 info: Try this:
-  simp only [Nat.add_comm]
+  [apply] simp only [Nat.add_comm]
 -/
 #guard_msgs in
 example : x + 1 = 1 + x := by simp? [Nat.add_comm, Nat.mul_comm]
 /--
 info: Try this:
-  dsimp only [Nat.reduceAdd]
+  [apply] dsimp only [Nat.reduceAdd]
 -/
 #guard_msgs in
 example : 1 + 1 = 2 := by dsimp?
@@ -27,10 +27,10 @@ example : 1 + 1 = 2 := by dsimp?
 
 /--
 info: Try this:
-  simp only [foo, bar]
+  [apply] simp only [foo, bar]
 ---
 info: Try this:
-  simp only [foo, baz]
+  [apply] simp only [foo, baz]
 -/
 #guard_msgs in
 example : foo x y = 1 + y := by
@@ -40,7 +40,7 @@ example : foo x y = 1 + y := by
 
 /--
 info: Try this:
-  simp only [foo, bar, baz]
+  [apply] simp only [foo, bar, baz]
 -/
 #guard_msgs in
 example : foo x y = 1 + y := by

BatteriesTest/simpa.lean

@@ -96,14 +96,14 @@ example (P : Bool) (h : ¬ ¬ P) : P := by
 
 /--
 info: Try this:
-  simpa only using h
+  [apply] simpa only using h
 -/
 #guard_msgs in
 example (p : Prop) (h : p) : p := by simpa? using h
 
 /--
 info: Try this:
-  simpa only [and_true] using h
+  [apply] simpa only [and_true] using h
 -/
 #guard_msgs in
 example (p : Prop) (h : p ∧ True) : p := by simpa? using h

BatteriesTest/tryThis.lean

@@ -62,18 +62,18 @@ private def s : Suggestion := Unhygienic.run `(tactic| rfl)
 
 /--
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 -- `Try this: rfl` with `rfl` in text-link color.
 #demo1 s
 
 /--
 info: Try these:
-  • rfl
-  • rfl
-  • rfl
-  • rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
 -/
 #guard_msgs in
 /-
@@ -94,13 +94,13 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Try these:
-  • rfl
-  • rfl
-  • rfl
-  • rfl
-  • rfl
-  • rfl
-  • rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
 -/
 #guard_msgs in
 /-
@@ -123,7 +123,7 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.error` has been deprecated: `
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.error` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 -- `Try this: rfl` -- error color, no squiggle
@@ -135,7 +135,7 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated:
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 -- `Try this: rfl` -- gold color with warning squiggle
@@ -147,7 +147,7 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated:
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 -- `Try this: rfl` -- gold color with no squiggle
@@ -159,7 +159,7 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.success` has been deprecated:
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.success` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 -- `Try this: rfl` -- Lean green
@@ -171,7 +171,7 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis` has been deprec
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 -- `Try this: rfl` -- styled like a goal hypothesis
@@ -183,32 +183,32 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible` has been depr
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 -- `Try this: rfl` -- styled like an inaccessible goal hypothesis
 #demo1 {s with style? := some .asInaccessible}
 
 /--
 info: Try this:
-  Starfleet
+  [apply] Starfleet
 -/
 #guard_msgs in
 -- `Try this: Starfleet`
 #demo1 {s with preInfo? := "Sta", postInfo? := "eet"}
 
 /--
 info: Try this:
-  a secret message
+  [apply] a secret message
 -/
 #guard_msgs in
 -- `Try this: a secret message`
 #demo1 {s with messageData? := m!"a secret message"}
 
 /--
 info: Try these:
-  • a secret message
-  • another secret message
+  [apply] a secret message
+  [apply] another secret message
 -/
 #guard_msgs in
 /-
@@ -225,17 +225,17 @@ Try these:
 
 /--
 info: Our only hope is ⏎
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 #demo1 s with_header "Our only hope is "
 
 /--
 info: We've got everything here! Such as:
-  • rfl
-  • rfl
-  • rfl
-  • rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
 -/
 #guard_msgs in
 #demo #[s,s,s,s] with_header "We've got everything here! Such as:"
@@ -258,11 +258,11 @@ warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `
 warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `SuggestionStyle` is not used anymore.
 ---
 info: Grab bag:
-  • This is not a tactic.
-  • This could be a tactic--but watch out!
-  • rfl. Finally, a tactic that just works.
-  • I'm just link-styled.
-  • On a scale of 0 to 1, I'd put this at 0.166667.
+  [apply] This is not a tactic.
+  [apply] This could be a tactic--but watch out!
+  [apply] rfl. Finally, a tactic that just works.
+  [apply] I'm just link-styled.
+  [apply] On a scale of 0 to 1, I'd put this at 0.166667.
 -/
 #guard_msgs in
 #demo #[
@@ -297,7 +297,7 @@ info: Grab bag:
 menu should read "Consider rfl, please" -/
 /--
 info: Try this:
-  rfl
+  [apply] rfl
 -/
 #guard_msgs in
 #demo1 { s with toCodeActionTitle? := fun text => "Consider " ++ text ++ ", please" }
@@ -315,9 +315,9 @@ macro "#demo" s:term "with_code_action_prefix" h:str : command => `(example : Tr
 menu should read "Maybe use: rfl"; "Maybe use: rfl"; "Also consider rfl, please!" -/
 /--
 info: Try these:
-  • rfl
-  • rfl
-  • rfl
+  [apply] rfl
+  [apply] rfl
+  [apply] rfl
 -/
 #guard_msgs in
 #demo #[