Def Lean.Name.isLocal

Modification history

2025-12-05 11:03
Mathlib/Tactic/Linter/UpstreamableDecl.lean
chore(Tactic/Linters): remove `public section` (#31803) …
Deleted Lean.Name.isLocalView on Github →
2024-11-18 11:19
Mathlib/Tactic/Linter/UpstreamableDecl.lean
feat: the upstreamDecl linter (#18702) …
Added Lean.Name.isLocalView on Github →