diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean index 8c8403d57e..e3786aeb46 100644 --- a/src/Lean/Compiler/LCNF/SpecInfo.lean +++ b/src/Lean/Compiler/LCNF/SpecInfo.lean @@ -189,7 +189,11 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do let mut paramsInfo := declsInfo[i]! let some mask := m.find? decl.name | unreachable! trace[Compiler.specialize.info] "{decl.name} {mask}" - paramsInfo := Array.zipWith (fun info fixed => if fixed || info matches .user then info else .other) paramsInfo mask + paramsInfo := Array.zipWith (as := paramsInfo) (bs := mask) fun info fixed => + if fixed || info matches .user then + info + else + .other for j in [:paramsInfo.size] do let mut info := paramsInfo[j]! if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then