From a1cf67edc333175e9c116301bb50eb6ba2d76943 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Tue, 19 Aug 2025 11:20:32 -0400
Subject: [PATCH] feat: parser alias for `visibility` (#9974)

This PR registers a parser alias for `Lean.Parser.Command.visibility`.
This avoids having to import `Lean.Parser.Command` in simple command
macros that use visibilities.
---
 src/Lean/Parser/Command.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 283442f023..ddbecce413 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -867,6 +867,7 @@ builtin_initialize
   register_parser_alias                                                 optDeclSig
   register_parser_alias                                                 openDecl
   register_parser_alias                                                 docComment
+  register_parser_alias                                                 visibility
 
 /--
 Registers an error explanation.