max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: parser alias for visibility (#9974)

Browse source 
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.
This commit is contained in:
Mac Malone 2025-08-19 11:20:32 -04:00 • committed by GitHub
parent d0167f7002
commit a1cf67edc3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Parser/Command.lean
View file

@ -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.