Skip to content

Commit 625b997

Browse files
committed
fix: make register_try?_tactic auxiliary definitions internal
The auxiliary definitions created by `register_try?_tactic` are internal implementation details that should not be visible to user-facing linters. This change marks them as internal by using `Name.mkSimpleInternal` instead of `Name.mkSimple`, which automatically exempts them from linting via the existing `isAutoDecl` check in Batteries. Fixes linter errors in downstream projects (e.g., Mathlib) when using `register_try?_tactic`. 🤖 Generated with Claude Code
1 parent 6cbcbce commit 625b997

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Elab/Tactic/Try.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -295,7 +295,7 @@ meta def elabRegisterTryTactic : Command.CommandElab := fun stx => do
295295

296296
-- Generate a unique name based on a hash of the tactic syntax
297297
let tacHash := hash tacStx.prettyPrint.pretty
298-
let name := Name.mkSimple s!"auxTryTactic{tacHash}"
298+
let name := Name.mkSimpleInternal s!"auxTryTactic{tacHash}"
299299

300300
-- Generate code that parses the tactic at runtime
301301
let prioStx := Syntax.mkNumLit (toString prio)

0 commit comments

Comments
 (0)