From 30a5f19f30bd99fdf7b8624a129be920c11dff7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2019 15:09:07 -0800 Subject: [PATCH] feat: simplify code using `filterRevM` cc @kha --- src/Init/Lean/Elab/Term.lean | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index cce5d63a40..8d05d07ac3 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -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