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

fix: incorrect FVarSubst for subst tactic

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-03 11:35:14 -07:00
parent 9746f8ab25
commit 252ef7345f
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -27,12 +27,14 @@ withMVarContext mvarId $ do
a ← whnf a;
match a with
| Expr.fvar aFVarId _ => do
trace! `Meta.Tactic.subst ("substituting " ++ a ++ " (id: " ++ aFVarId ++ ") with " ++ b);
mctx ← getMCtx;
when (mctx.exprDependsOn b aFVarId) $
throwTacticEx `subst mvarId ("'" ++ a ++ "' occurs at" ++ indentExpr b);
aLocalDecl ← getLocalDecl aFVarId;
(vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true;
(twoVars, mvarId) ← introN mvarId 2 [] false;
trace! `Meta.Tactic.subst ("reverted variables " ++ toString vars);
let aFVarId := twoVars.get! 0;
let a := mkFVar aFVarId;
let hFVarId := twoVars.get! 1;
@ -59,7 +61,7 @@ withMVarContext mvarId $ do
(newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false;
fvarSubst ← newFVars.size.foldM
(fun i (fvarSubst : FVarSubst) =>
let var := vars.get! i;
let var := vars.get! (i+2);
let newFVar := newFVars.get! i;
pure $ fvarSubst.insert var newFVar)
FVarSubst.empty;