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

chore: improve readability of a zipWith call (#9116)

Browse source
This commit is contained in:
Cameron Zwarich 2025-06-30 17:10:54 -07:00 • committed by GitHub
parent 52ab0141cd
commit 463f2c5f25
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Compiler/LCNF/SpecInfo.lean
View file

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