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

fix: Tactic failure on synthesizing placeholder #139

Merged
aniva merged 10 commits from bug/tactic-failure-placeholder into dev 2024-12-11 01:13:15 -08:00
Conversation 4 Commits 10 Files Changed 4 +1 -6
1 changed files with 1 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit e0e5c9ec68 - Show all commits

7
Pantograph/Goal.lean
View File

@ -186,8 +186,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src) let descendants ← Meta.getMVars $ ← instantiateMVars (.mvar src)
let mut alreadyVisited : MVarIdSet := {} let mut alreadyVisited : MVarIdSet := {}
let mut result : MVarIdSet := {} let mut result : MVarIdSet := {}
for mvarErrorInfo in (← get).mvarErrorInfos do for { mvarId, .. } in (← get).mvarErrorInfos do
let mvarId := mvarErrorInfo.mvarId
unless alreadyVisited.contains mvarId do unless alreadyVisited.contains mvarId do
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
@ -196,10 +195,6 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
if mvarDeps.any descendants.contains then do if mvarDeps.any descendants.contains then do
result := result.insert mvarId result := result.insert mvarId
return result.toList return result.toList
--(← getThe Elab.Term.State).mvarErrorInfos
-- |>.map (·.mvarId)
-- |>.filterM λ mvarId =>
-- return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId := private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
let li2' := li2.filter (¬ li1.contains ·) let li2' := li2.filter (¬ li1.contains ·)