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

chore: improve error messages

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-20 14:22:01 -07:00
parent faa59ead97
commit dcd3068b42
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Tactic/Rewrite.lean
View file

@ -24,7 +24,7 @@ withMVarContext mvarId do
let heq := mkAppN heq newMVars
let cont (heq heqType : Expr) : MetaM RewriteResult :=
match heqType.eq? with
| none => throwTacticEx `rewrite mvarId "equality of iff proof expected"
| none => throwTacticEx `rewrite mvarId msg!"equality of iff proof expected{indentExpr heqType}"
| some (α, lhs, rhs) =>
let cont (heq heqType lhs rhs : Expr) : MetaM RewriteResult := do
if lhs.getAppFn.isMVar then
@ -32,7 +32,7 @@ withMVarContext mvarId do
let e ← instantiateMVars e
let eAbst ← kabstract e lhs occs
unless eAbst.hasLooseBVars do
throwTacticEx `rewrite mvarId "did not find instance of the pattern in the target expression"
throwTacticEx `rewrite mvarId msg!"did not find instance of the pattern in the target expression{indentExpr lhs}"
-- construct rewrite proof
let eNew := eAbst.instantiate1 rhs
let eNew ← instantiateMVars eNew