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

feat: docComment parser alias

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-22 13:28:37 +02:00
parent a10a5335ba
commit 8e07e80f72
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

@ -153,6 +153,7 @@ builtin_initialize
register_parser_alias declVal
register_parser_alias optDeclSig
register_parser_alias openDecl
register_parser_alias docComment
end Command