Skip to content

Commit d696472

Browse files
committed
Add tactic alt tags.
1 parent 5e24e12 commit d696472

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

Mathlib/Tactic/Convert.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -274,6 +274,7 @@ pattern-matched, like `rintro` would, using the `with` keyword.
274274
syntax (name := convertTo) "convert_to" ("!")? Parser.Tactic.optConfig " ←"? ppSpace term
275275
(" using " num)? (" with" (ppSpace colGt rintroPat)*)? (Parser.Tactic.location)? : tactic
276276

277+
@[tactic_alt convertTo]
277278
syntax (name := convert_to!) "convert_to!" Lean.Parser.Tactic.optConfig " ←"? ppSpace term
278279
(" using " num)? (" with" (ppSpace colGt rintroPat)*)? (Parser.Tactic.location)? : tactic
279280

0 commit comments

Comments
 (0)