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

chore: remove dead variable

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-10 13:41:55 -07:00
parent 2a676b6dfb
commit e49dfccc2a
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Elab/Tactic/Rewrite.lean
View file

@ -50,7 +50,6 @@ def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do
let loc := expandOptLocation stx[2]
-- show initial state up to (incl.) `[`
withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
let mut newTacs := #[]
let numRules := (rules.size + 1) / 2
for i in [:numRules] do
let rule := rules[i * 2]