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

fix: typo at copyDefaultValue?

Browse source 
see #1190
This commit is contained in:
Leonardo de Moura 2022-06-06 07:57:23 -07:00
parent 22281f25c8
commit d00d8a2104
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/Structure.lean
View file

@ -388,7 +388,7 @@ where
go? (b.instantiate1 arg)
| e =>
let r := if e.isAppOfArity ``id 2 then e.appArg! else e
return some (← reduceProjs (← instantiateMVars e.appArg!) expandedStructNames)
return some (← reduceProjs (← instantiateMVars r) expandedStructNames)
private partial def copyNewFieldsFrom (structDeclName : Name) (infos : Array StructFieldInfo) (parentType : Expr) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
copyFields infos {} parentType fun infos _ _ => k infos