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

fix: improved error span for inherit_doc (#1807)

Browse source
This commit is contained in:
Mario Carneiro 2022-11-07 21:11:41 +01:00 • committed by GitHub
parent cf35416f5b
commit 22cdac914d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/InheritDoc.lean
View file

@ -16,12 +16,12 @@ builtin_initialize
unless kind == AttributeKind.global do
throwError "invalid `[inherit_doc]` attribute, must be global"
match stx with
| `(attr| inherit_doc $[$id?:ident]?) =>
| `(attr| inherit_doc $[$id?:ident]?) => withRef stx[0] do
let some id := id?
| throwError "invalid `[inherit_doc]` attribute, could not infer doc source"
let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id
if (← findDocString? (← getEnv) decl).isSome then
logWarningAt id m!"{← mkConstWithLevelParams decl} already has a doc string"
logWarning m!"{← mkConstWithLevelParams decl} already has a doc string"
let some doc ← findDocString? (← getEnv) declName
| logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
addDocString decl doc