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

feat: simplify code using filterRevM

Browse source 
cc @kha
This commit is contained in:
Leonardo de Moura 2019-12-19 15:09:07 -08:00
parent 40f7caca0b
commit 30a5f19f30
1 changed files with 1 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Lean/Elab/Term.lean
View file

@ -572,14 +572,6 @@ match mvarSyntheticDecl.kind with
| SyntheticMVarKind.postponed macroStack => resumePostponed macroStack mvarSyntheticDecl.ref mvarSyntheticDecl.mvarId
| SyntheticMVarKind.tactic tacticCode => throwError tacticCode "not implemented yet"
/-- Auxiliary function for `synthesizeSyntheticMVarsStep`. -/
private def synthesizeSyntheticMVarsStepAux : List SyntheticMVarDecl → List SyntheticMVarDecl → TermElabM (List SyntheticMVarDecl)
| [], remaining => pure remaining
| mvarDecl :: mvarDecls, remaining =>
condM (synthesizeSyntheticMVar mvarDecl)
(synthesizeSyntheticMVarsStepAux mvarDecls remaining)
(synthesizeSyntheticMVarsStepAux mvarDecls (mvarDecl :: remaining))
/--
Try to synthesize the current list of pending synthetic metavariables.
Return `true` if it managed to synthesize at least one of them. -/
@ -588,7 +580,7 @@ s ← get;
let syntheticMVars := s.syntheticMVars.reverse;
let numSyntheticMVars := syntheticMVars.length;
modify $ fun s => { syntheticMVars := [], .. s };
remainingSyntheticMVars ← synthesizeSyntheticMVarsStepAux syntheticMVars [];
remainingSyntheticMVars ← syntheticMVars.filterRevM $ fun mvarDecl => not <$> synthesizeSyntheticMVar mvarDecl;
modify $ fun s => { syntheticMVars := s.syntheticMVars ++ remainingSyntheticMVars, .. s };
pure $ numSyntheticMVars != remainingSyntheticMVars.length