chore: improve error message

2020-08-07 11:50:08 -07:00 · 2020-08-07 11:50:08 -07:00 · feda5e746f
commit feda5e746f
parent aefc9a473f
1 changed files with 1 additions and 0 deletions
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@ -103,6 +103,7 @@ withMVarContext mvarId $ do
        "invalid equality proof, it is not of the form "
        ++ (if symm then "(t = x)" else "(x = t)")
        ++ indentExpr hLocalDecl.type
+        ++ Format.line ++ "after WHNF, variable expected, but obtained" ++ indentExpr a

 def subst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId :=
 withMVarContext mvarId $ do