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

feat: improve tagUntaggedGoals

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-30 16:35:00 -07:00
parent 6ff03d7301
commit 48cef717aa
1 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Elab/Tactic/Basic.lean
View file

@ -228,18 +228,20 @@ focusAux (do a ← tactic; done; pure a)
/--
Use `parentTag` to tag untagged goals at `newGoals`.
If there are multiple new goals, they are named using `<parentTag>.<newSuffix>_<idx>` where `idx > 0`.
If there is only one new goal, then we just use `parentTag` -/
If there are multiple new untagged goals, they are named using `<parentTag>.<newSuffix>_<idx>` where `idx > 0`.
If there is only one new untagged goal, then we just use `parentTag` -/
def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
mctx ← getMCtx;
match newGoals with
| [g] => modifyMCtx $ fun mctx => if mctx.isAnonymousMVar g then mctx.renameMVar g parentTag else mctx
| _ => modifyMCtx $ fun mctx =>
let numAnonymous := newGoals.foldl (fun n g => if mctx.isAnonymousMVar g then n + 1 else n) 0;
modifyMCtx fun mctx =>
let (mctx, _) := newGoals.foldl
(fun (acc : MetavarContext × Nat) (g : MVarId) =>
let (mctx, idx) := acc;
if mctx.isAnonymousMVar g then
(mctx.renameMVar g (parentTag ++ newSuffix.appendIndexAfter idx), idx+1)
if numAnonymous == 1 then
(mctx.renameMVar g parentTag, idx+1)
else
(mctx.renameMVar g (parentTag ++ newSuffix.appendIndexAfter idx), idx+1)
else
acc)
(mctx, 1);