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

docs: fix doc comment syntax in declModifiers doc comment (#2590)

Browse source 
The hover on `declModifiers` says doc comments are `/-! … -/`, when it
should say `/-- … -/`.
This commit is contained in:
Joachim Breitner 2023-09-27 03:57:40 +02:00 • committed by GitHub
parent e6fe3bee71
commit ae470e038e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -72,7 +72,7 @@ def «partial» := leading_parser "partial "
def «nonrec» := leading_parser "nonrec "
/-- `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-! ... -/`
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`

2
tests/lean/interactive/hover.lean.expected.out
View file

@ -374,7 +374,7 @@
{"start": {"line": 194, "character": 0}, "end": {"line": 194, "character": 9}},
"contents":
{"value":
"`declModifiers` is the collection of modifiers on a declaration:\n* a doc comment `/-! ... -/`\n* a list of attributes `@[attr1, attr2]`\n* a visibility specifier, `private` or `protected`\n* `noncomputable`\n* `unsafe`\n* `partial` or `nonrec`\n\nAll modifiers are optional, and have to come in the listed order.\n\n`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed\non the same line as the declaration. It is used for declarations nested inside other syntax,\nsuch as inductive constructors, structure projections, and `let rec` / `where` definitions. ",
"`declModifiers` is the collection of modifiers on a declaration:\n* a doc comment `/-- ... -/`\n* a list of attributes `@[attr1, attr2]`\n* a visibility specifier, `private` or `protected`\n* `noncomputable`\n* `unsafe`\n* `partial` or `nonrec`\n\nAll modifiers are optional, and have to come in the listed order.\n\n`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed\non the same line as the declaration. It is used for declarations nested inside other syntax,\nsuch as inductive constructors, structure projections, and `let rec` / `where` definitions. ",
"kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 200, "character": 2}}