From 96ddeea84e0f2762b3abab437c68a153a3c57d27 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 30 Mar 2025 21:27:13 -0700 Subject: [PATCH] fix: fix FieldInfo for structure instance notation (#7745) This PR fixes an oversight in #7717, and now fields get a FieldInfo node with the correct projection function. Note that for copied fields "go to definition" still does not go anywhere, since copied projection function has no declaration range. We probably should make such fields instead go to the origin projection function. --- src/Lean/Elab/StructInst.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index e678cfd90a..190636ee8f 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -702,10 +702,12 @@ private def addStructFieldAux (fieldName : Name) (e : Expr) : StructInstM Unit : private def addStructField (fieldView : ExpandedField) (e : Expr) : StructInstM Unit := do let fieldName := fieldView.name addStructFieldAux fieldName e - let projName := (← read).structName ++ fieldName - pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo { - projName, fieldName, lctx := (← getLCtx), val := e, stx := fieldView.ref - } + let env ← getEnv + if let some structName := findField? env (← read).structName fieldName then + if let some fieldInfo := getFieldInfo? env structName fieldName then + pushInfoTree <| InfoTree.node (children := {}) <| Info.ofFieldInfo { + projName := fieldInfo.projFn, fieldName, lctx := (← getLCtx), val := e, stx := fieldView.ref + } private def elabStructField (_fieldName : Name) (stx : Term) (fieldType : Expr) : StructInstM Expr := do let fieldType ← normalizeExpr fieldType