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

fix: must set mvar as natural

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-08 18:49:33 -08:00
parent 7a556d8f61
commit da2e5b6fdf
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/Init/Lean/Meta/Tactic/Revert.lean
View file

@ -13,7 +13,9 @@ def revert (mvarId : MVarId) (fvars : Array FVarId) : MetaM (Array FVarId × MVa
if fvars.isEmpty then pure (fvars, mvarId)
else withMVarContext mvarId $ do
checkNotAssigned mvarId `revert;
e ← elimMVarDeps (fvars.map mkFVar) (mkMVar mvarId);
-- Set metavariable kind to natural to make sure `elimMVarDeps` will assign it.
setMVarKind mvarId MetavarKind.natural;
e ← finally (elimMVarDeps (fvars.map mkFVar) (mkMVar mvarId)) (setMVarKind mvarId MetavarKind.syntheticOpaque);
pure $ e.withApp $ fun mvar args => (args.map Expr.fvarId!, mvar.mvarId!)
end Meta