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

fix: fix FieldInfo for structure instance notation (#7745)

Browse source 
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.
This commit is contained in:
Kyle Miller 2025-03-30 21:27:13 -07:00 • committed by GitHub
parent c8ee006f91
commit 96ddeea84e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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