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

fix: one more struct instance syntax manipulation

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-16 13:33:06 +02:00
parent 0f6e6c8a51
commit 6982536108
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/StructInst.lean
View file

@ -184,7 +184,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sources : Array ExplicitSource
let valField := modifyOp.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[valFirst, valRest]
let valSource := mkSourcesWithSyntax #[s]
let val := stx.setArg 1 valSource
let val := val.setArg 2 <| mkNullNode #[mkNullNode #[valField, mkNullNode]]
let val := val.setArg 2 <| mkNullNode #[valField]
trace[Elab.struct.modifyOp] "{stx}\nval: {val}"
cont val