From c10230ec0a201096da6736d769f3066da0e4d5bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Mar 2020 15:37:04 -0700 Subject: [PATCH] feat: add `elabTermAndSynthesize` auxiliary method Useful for creating "checkpoints". --- src/Init/Lean/Elab/SyntheticMVars.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Init/Lean/Elab/SyntheticMVars.lean b/src/Init/Lean/Elab/SyntheticMVars.lean index 688baf4901..5f0e7f684e 100644 --- a/src/Init/Lean/Elab/SyntheticMVars.lean +++ b/src/Init/Lean/Elab/SyntheticMVars.lean @@ -211,6 +211,18 @@ private partial def synthesizeSyntheticMVarsAux (mayPostpone := true) : Unit → def synthesizeSyntheticMVars (mayPostpone := true) : TermElabM Unit := synthesizeSyntheticMVarsAux mayPostpone () +/-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/ +def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do +s ← get; +let syntheticMVars := s.syntheticMVars; +modify $ fun s => { syntheticMVars := [], .. s }; +finally + (do + v ← elabTerm stx expectedType?; + synthesizeSyntheticMVars false; + instantiateMVars stx v) + (modify $ fun s => { syntheticMVars := s.syntheticMVars ++ syntheticMVars, .. s }) + end Term end Elab end Lean