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

fix: missing synthesizeSyntheticMVars at elabSubst

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-06 16:15:29 -07:00
parent aa9167834b
commit ab16278ce4
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/BuiltinNotation.lean
View file

@ -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