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

feat: make structure type clickable in “not a field” error (#5072)

Browse source
This commit is contained in:
Joachim Breitner 2024-08-16 11:06:18 +02:00 • committed by GitHub
parent cd21687884
commit 72f2e7aab1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/StructInst.lean
View file

@ -9,6 +9,7 @@ import Lean.Parser.Term
import Lean.Meta.Structure
import Lean.Elab.App
import Lean.Elab.Binders
import Lean.PrettyPrinter
namespace Lean.Elab.Term.StructInst
@ -433,7 +434,7 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
| { lhs := .fieldName ref fieldName :: _, .. } =>
addCompletionInfo <| CompletionInfo.fieldId ref fieldName (← getLCtx) s.structName
match findField? env s.structName fieldName with
| none => throwErrorAt ref "'{fieldName}' is not a field of structure '{s.structName}'"
| none => throwErrorAt ref "'{fieldName}' is not a field of structure '{MessageData.ofConstName s.structName}'"
| some baseStructName =>
if baseStructName == s.structName then pure field
else match getPathToBaseStructure? env baseStructName s.structName with