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

chore: improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-18 15:23:28 -07:00
parent 43bc429abf
commit f7bd174bb8
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -13,10 +13,10 @@ namespace Meta
structure RewriteResult :=
(eNew : Expr)
(eqPrf : Expr)
(newGoals : List MVarId)
(eqProof : Expr)
(mvarIds : List MVarId) -- new goals
def rewriteCore (mvarId : MVarId) (e : Expr) (heq : Expr) (symm : Bool := false) (occs : Occurrences := Occurrences.all) : MetaM RewriteResult :=
def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) (symm : Bool := false) (occs : Occurrences := Occurrences.all) : MetaM RewriteResult :=
withMVarContext mvarId $ do
checkNotAssigned mvarId `rewrite;
heqType ← inferType heq;
@ -28,7 +28,7 @@ withMVarContext mvarId $ do
| some (α, lhs, rhs) =>
let continue (heq heqType lhs rhs : Expr) : MetaM RewriteResult := do {
when lhs.getAppFn.isMVar $
throwTacticEx `rewrite mvarId ("pattern is a metavariable");
throwTacticEx `rewrite mvarId ("pattern is a metavariable " ++ indentExpr lhs ++ Format.line ++ "from equation" ++ indentExpr heqType);
e ← instantiateMVars e;
eAbst ← kabstract e lhs occs;
unless eAbst.hasLooseBVars $
@ -45,7 +45,7 @@ withMVarContext mvarId $ do
eqPrf ← mkEqNDRec motive eqRefl heq;
postprocessAppMVars `rewrite mvarId newMVars binderInfos;
newMVars ← newMVars.filterM $ fun mvar => not <$> isExprMVarAssigned mvar.mvarId!;
pure { eNew := eNew, eqPrf := eqPrf, newGoals := newMVars.toList.map Expr.mvarId! }
pure { eNew := eNew, eqProof := eqPrf, mvarIds := newMVars.toList.map Expr.mvarId! }
};
match symm with
| false => continue heq heqType lhs rhs