From ab16278ce4b030c7d98cea6bf2a31b66eeb332b2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jul 2022 16:15:29 -0700 Subject: [PATCH] fix: missing `synthesizeSyntheticMVars` at `elabSubst` --- src/Lean/Elab/BuiltinNotation.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index eb4e4f4687..8abc77d4e6 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -304,7 +304,8 @@ See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lea let expectedType? ← tryPostponeIfHasMVars? expectedType? match stx with | `($heqStx ▸ $hStx) => do - let mut heq ← elabTerm heqStx none + synthesizeSyntheticMVars + let mut heq ← withSynthesize <| elabTerm heqStx none let heqType ← inferType heq let heqType ← instantiateMVars heqType match (← Meta.matchEq? heqType) with @@ -322,7 +323,7 @@ See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lea unless expectedAbst.hasLooseBVars do expectedAbst ← kabstract expectedType lhs unless expectedAbst.hasLooseBVars do - throwError "invalid `▸` notation, expected result type of cast is {indentExpr expectedType}\n.However, the equality {indentExpr heq}\nof type {indentExpr heqType}\ndoes not contain the expected result type on either the left or the right hand side" + throwError "invalid `▸` notation, expected result type of cast is {indentExpr expectedType}\nhowever, the equality {indentExpr heq}\nof type {indentExpr heqType}\ndoes not contain the expected result type on either the left or the right hand side" heq ← mkEqSymm heq (lhs, rhs) := (rhs, lhs) let hExpectedType := expectedAbst.instantiate1 lhs