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

doc: fix typo in error message (#7807)

Browse source 
I encountered this error message typo recently.
This commit is contained in:
JovanGerb 2025-04-04 01:40:11 +01:00 • committed by GitHub
parent 092ece5d49
commit 906edd4529
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Term.lean
View file

@ -1950,7 +1950,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
if let some (e, projs) ← resolveLocalName n then
unless explicitLevels.isEmpty do
throwError "invalid use of explicit universe parameters, '{e}' is a local"
throwError "invalid use of explicit universe parameters, '{e}' is a local variable"
return [(e, projs)]
let preresolved := preresolved.filterMap fun
| .decl n projs => some (n, projs)