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

chore: minor cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-17 16:47:30 -08:00
parent 6263141f7b
commit ea26caa3fa
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -28,13 +28,13 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
let holeName := mkIdentFrom holeOrTacticSeq tag
let newHole ← `(?$holeName:ident)
modify fun s => { s with nextIdx := s.nextIdx + 1}
pure $ alt.setArg 3 newHole
pure <| alt.setArg 3 newHole
else withFreshMacroScope do
let newHole ← `(?rhs)
let newHoleId := newHole[1]
let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
modify fun s => { s with cases := s.cases.push newCase }
pure $ alt.setArg 3 newHole
pure <| alt.setArg 3 newHole
let result := matchTac.setKind ``Parser.Term.«match»
let result := result.setArg 4 (mkNode ``Parser.Term.matchAlts #[mkNullNode newAlts])
pure result
@ -46,9 +46,9 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
@[builtinTactic Lean.Parser.Tactic.match]
def evalMatch : Tactic := fun stx => do
let tag ← getMainTag
let (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm tag stx
let (matchTerm, cases) ← liftMacroM <| mkAuxiliaryMatchTerm tag stx
let refineMatchTerm ← `(tactic| refine $matchTerm)
let stxNew := mkNullNode (#[refineMatchTerm] ++ cases)
withMacroExpansion stx stxNew $ evalTactic stxNew
withMacroExpansion stx stxNew <| evalTactic stxNew
end Lean.Elab.Tactic