Try even more postponing.

leanprover-community · Jul 17, 2023 · 530b35c · 530b35c
1 parent e861ebb
commit 530b35c
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
@@ -463,6 +463,7 @@ def Impl.macro (t : Syntax) (expectedType : Expr) : TermElabM Expr := do
     if ← synth.isAssigned then
       let t ← synth.synth s
       unless ← isDefEq mvar t do
+        tryPostpone
         throwError "cannot assign metavariable ({mvar} : {← inferType mvar}) with {t}"
 
   instantiateMVars mainMVar