fix: preprocessLCtx (#12081)

This PR fixes a bug in the `Sym.preprocessLCtx` function.
This commit is contained in:
Leonardo de Moura 2026-01-21 06:05:43 -08:00 committed by GitHub
parent 94e8fd4845
commit 8258cfe2a1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -74,6 +74,7 @@ def preprocessLCtx (lctx : LocalContext) : SymM LocalContext := do
let type ← preprocessExpr type
let value ← preprocessExpr value
pure <| LocalDecl.ldecl index fvarId userName type value nondep kind
index := index + 1
decls := decls.push (some decl)
fvarIdToDecl := fvarIdToDecl.insert decl.fvarId decl
return { fvarIdToDecl, decls, auxDeclToFullName }