From 72f2e7aab1e041e361c0be39cc90751f91f8d6f0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 16 Aug 2024 11:06:18 +0200 Subject: [PATCH] =?UTF-8?q?feat:=20make=20structure=20type=20clickable=20i?= =?UTF-8?q?n=20=E2=80=9Cnot=20a=20field=E2=80=9D=20error=20(#5072)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Lean/Elab/StructInst.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 4bd8b71d52..220d7b8e91 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -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