Skip to content

Commit 3b6972c

Browse files
kim-emclaude
andcommitted
chore: deduplicate SuggestionStyle deprecation warnings in tryThis test
Lean now emits each `SuggestionStyle` deprecation warning once instead of twice per source location. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 2941ca9 commit 3b6972c

File tree

1 file changed

+0
-22
lines changed

1 file changed

+0
-22
lines changed

BatteriesTest/tryThis.lean

Lines changed: 0 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -91,8 +91,6 @@ with `rfl` in text-link color.
9191
/--
9292
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `SuggestionStyle` is not used anymore.
9393
---
94-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `SuggestionStyle` is not used anymore.
95-
---
9694
info: Try these:
9795
[apply] rfl
9896
[apply] rfl
@@ -120,8 +118,6 @@ Try these:
120118
/--
121119
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.error` has been deprecated: `SuggestionStyle` is not used anymore.
122120
---
123-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.error` has been deprecated: `SuggestionStyle` is not used anymore.
124-
---
125121
info: Try this:
126122
[apply] rfl
127123
-/
@@ -132,8 +128,6 @@ info: Try this:
132128
/--
133129
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
134130
---
135-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
136-
---
137131
info: Try this:
138132
[apply] rfl
139133
-/
@@ -144,8 +138,6 @@ info: Try this:
144138
/--
145139
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
146140
---
147-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
148-
---
149141
info: Try this:
150142
[apply] rfl
151143
-/
@@ -156,8 +148,6 @@ info: Try this:
156148
/--
157149
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.success` has been deprecated: `SuggestionStyle` is not used anymore.
158150
---
159-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.success` has been deprecated: `SuggestionStyle` is not used anymore.
160-
---
161151
info: Try this:
162152
[apply] rfl
163153
-/
@@ -168,8 +158,6 @@ info: Try this:
168158
/--
169159
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis` has been deprecated: `SuggestionStyle` is not used anymore.
170160
---
171-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis` has been deprecated: `SuggestionStyle` is not used anymore.
172-
---
173161
info: Try this:
174162
[apply] rfl
175163
-/
@@ -180,8 +168,6 @@ info: Try this:
180168
/--
181169
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible` has been deprecated: `SuggestionStyle` is not used anymore.
182170
---
183-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible` has been deprecated: `SuggestionStyle` is not used anymore.
184-
---
185171
info: Try this:
186172
[apply] rfl
187173
-/
@@ -243,20 +229,12 @@ info: We've got everything here! Such as:
243229
/--
244230
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.error` has been deprecated: `SuggestionStyle` is not used anymore.
245231
---
246-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.error` has been deprecated: `SuggestionStyle` is not used anymore.
247-
---
248232
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
249233
---
250-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.warning` has been deprecated: `SuggestionStyle` is not used anymore.
251-
---
252-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.success` has been deprecated: `SuggestionStyle` is not used anymore.
253-
---
254234
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.success` has been deprecated: `SuggestionStyle` is not used anymore.
255235
---
256236
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `SuggestionStyle` is not used anymore.
257237
---
258-
warning: `Lean.Meta.Tactic.TryThis.SuggestionStyle.value` has been deprecated: `SuggestionStyle` is not used anymore.
259-
---
260238
info: Grab bag:
261239
[apply] This is not a tactic.
262240
[apply] This could be a tactic--but watch out!

0 commit comments

Comments
 (0)