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

chore: improve trace message

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-29 16:54:48 -08:00
parent c14ded6984
commit 527c3c73b4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Term.lean
View file

@ -590,7 +590,7 @@ modify $ fun s => { syntheticMVars := [], .. s };
-- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
-- It would not be incorrect to use `filterM`.
remainingSyntheticMVars ← syntheticMVars.filterRevM $ fun mvarDecl => do {
trace `Elab.postpone mvarDecl.ref $ fun _ => fmt "resuming";
trace `Elab.postpone mvarDecl.ref $ fun _ => "resuming ?" ++ mvarDecl.mvarId;
succeeded ← synthesizeSyntheticMVar mvarDecl;
trace `Elab.postpone mvarDecl.ref $ fun _ => if succeeded then fmt "succeeded" else fmt "not ready yet";
pure $ !succeeded