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

fix: append match_<idx> suffix only there is more than one alternative

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-03 10:53:47 -08:00
parent b9a2885e65
commit f28a7306f2
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Tactic/Match.lean
View file

@ -23,7 +23,8 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
pure alt
else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
let s ← get
let holeName := mkIdentFrom holeOrTacticSeq (parentTag ++ (`match).appendIndexAfter s.nextIdx)
let tag := if alts.size > 1 then parentTag ++ (`match).appendIndexAfter s.nextIdx else parentTag
let holeName := mkIdentFrom holeOrTacticSeq tag
let newHole ← `(?$holeName:ident)
modify fun s => { s with nextIdx := s.nextIdx + 1}
pure $ alt.setArg 2 newHole