Skip to content

Commit 7111187

Browse files
committed
Forgot a @[tactic_alt]
1 parent 381a876 commit 7111187

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
@@ -296,6 +296,7 @@ example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
296296
```
297297
-/
298298
syntax (name := acChange) "ac_change " term (" using " num)? : tactic
299+
@[tactic_alt acChange]
299300
syntax (name := acChange!) "ac_change! " term (" using " num)? : tactic
300301

301302
macro_rules

0 commit comments

Comments
 (0)