aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

fix: Translate fvars in pending context

This commit is contained in:
Leni Aniva 2024-10-08 14:28:35 -07:00
parent 420e863756
commit 0e8c9f890b
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Pantograph/Frontend/MetaTranslate.lean
View File

@ -106,8 +106,9 @@ partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
let mvar' ← Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName let mvar' ← Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
let mvarId' := mvar'.mvarId! let mvarId' := mvar'.mvarId!
if let .some { fvars, mvarIdPending }:= (← getSourceMCtx).getDelayedMVarAssignmentExp srcMVarId then if let .some { fvars, mvarIdPending }:= (← getSourceMCtx).getDelayedMVarAssignmentExp srcMVarId then
let fvars' ← fvars.mapM translateExpr -- Map the fvars in the pending context.
let mvarIdPending' ← translateMVarId mvarIdPending let mvarIdPending' ← translateMVarId mvarIdPending
let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
assignDelayedMVar mvarId' fvars' mvarIdPending' assignDelayedMVar mvarId' fvars' mvarIdPending'
pure mvarId' pure mvarId'
addTranslatedMVar srcMVarId mvarId' addTranslatedMVar srcMVarId mvarId'