Skip to content

Commit e12bcd0

Browse files
committed
chore(Archive): make the macro local (leanprover-community#39367)
`◾` is [listed as the final tactic](https://leanprover-community.github.io/mathlib4_docs/tactics.html#%C2%ABtactic%E2%97%BE%C2%BB) provided by Mathlib, but it's just a synonym for `aesop` used in one `Archive` file, not actually for downstream consumption. By making it a local macro, it won't show up in the documentation page. Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
1 parent 146974d commit e12bcd0

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Archive/Examples/IfNormalization/Result.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,8 @@ import Mathlib.Tactic.Recall
1313
See `Statement.lean` for background.
1414
-/
1515

16-
macro "◾" : tactic => `(tactic| aesop)
17-
macro "◾" : term => `(term| by aesop)
16+
local macro "◾" : tactic => `(tactic| aesop)
17+
local macro "◾" : term => `(term| by aesop)
1818

1919
namespace IfExpr
2020

0 commit comments

Comments
 (0)