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

fix: Insert `mvarDeps`

This commit is contained in:
Leni Aniva 2024-12-11 00:16:52 -08:00
parent e0e5c9ec68
commit cb87fcd9dd
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Pantograph/Goal.lean
View File

@ -184,6 +184,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
-- was executing on `src`. `evalTactic`, will not capture these mvars, so we -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
-- need to manually find them and save them into the goal list. -- need to manually find them and save them into the goal list.
let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src) let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src)
--let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
let mut alreadyVisited : MVarIdSet := {} let mut alreadyVisited : MVarIdSet := {}
let mut result : MVarIdSet := {} let mut result : MVarIdSet := {}
for { mvarId, .. } in (← get).mvarErrorInfos do for { mvarId, .. } in (← get).mvarErrorInfos do
@ -191,9 +192,9 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
alreadyVisited := alreadyVisited.insert mvarId alreadyVisited := alreadyVisited.insert mvarId
/- The metavariable `mvarErrorInfo.mvarId` may have been assigned or /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
delayed assigned to another metavariable that is unassigned. -/ delayed assigned to another metavariable that is unassigned. -/
let mvarDeps ← Meta.getMVars (mkMVar mvarId) let mvarDeps ← Meta.getMVars (.mvar mvarId)
if mvarDeps.any descendants.contains then do if mvarDeps.any descendants.contains then do
result := result.insert mvarId result := mvarDeps.foldl (·.insert ·) result
return result.toList return result.toList
private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId := private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=