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

fix: preserveOrder logic

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-09 19:01:12 -08:00
parent 8d97b7c72e
commit 4d20fc8b5a
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Lean/MetavarContext.lean
View file

@ -710,11 +710,11 @@ else do
throw (Exception.revertFailure mctx lctx toRevert prevDecl)
};
let newToRevert := if preserveOrder then toRevert else Array.mkEmpty toRevert.size;
let firstDeclToVisit := if preserveOrder then lctx.getFVar! toRevert.back else getLocalDeclWithSmallestIdx lctx toRevert;
let skipFirst := preserveOrder;
let firstDeclToVisit := getLocalDeclWithSmallestIdx lctx toRevert;
let initSize := newToRevert.size;
lctx.foldlFromM
(fun (newToRevert : Array Expr) decl =>
if skipFirst && decl.index == firstDeclToVisit.index then pure newToRevert
if initSize.any $ fun i => decl.fvarId == (newToRevert.get! i).fvarId! then pure newToRevert
else if toRevert.any (fun x => decl.fvarId == x.fvarId!) then
pure (newToRevert.push decl.toExpr)
else if findLocalDeclDependsOn mctx decl (fun fvarId => newToRevert.any $ fun x => x.fvarId! == fvarId) then