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

fix: bug at FVarSubst generation

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-03 17:47:24 -07:00
parent e43b5e27a1
commit 8aa375ba3e
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/Tactic/Induction.lean
View file

@ -103,7 +103,7 @@ private partial def finalizeAux
(extra, mvarId') ← introN mvarId' nextra [] false;
let subst := reverted.size.fold
(fun i (subst : FVarSubst) =>
if i ≤ indices.size + 1 then subst
if i < indices.size + 1 then subst
else
let revertedFVarId := reverted.get! i;
let newFVarId := extra.get! (i - indices.size - 1);
@ -173,6 +173,7 @@ withMVarContext mvarId $ do
(majorFVarId', mvarId) ← intro1 mvarId false;
-- Create FVarSubst with indices
let baseSubst : FVarSubst := indices.iterate {} (fun i index subst => subst.insert index.fvarId! (indices'.get! i.val));
trace! `Meta.Tactic.induction ("after revert&intro" ++ Format.line ++ MessageData.ofGoal mvarId);
-- Update indices and major
let indices := indices'.map mkFVar;
let majorFVarId := majorFVarId';
@ -209,5 +210,8 @@ withMVarContext mvarId $ do
| _ =>
throwTacticEx `induction mvarId "major premise is not of the form (C ...)"
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Meta.Tactic.induction
end Meta
end Lean