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

chore: add optional preprocessing tactic

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-07 12:03:54 -08:00
parent 5d56e18811
commit dfa5cf9282
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Notation.lean
View file

@ -273,7 +273,7 @@ syntax (name := «let!») "let! " letDecl : tactic
syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
syntax inductionAlt := "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
syntax inductionAlts := "with " withPosition( (colGe inductionAlt)+)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic
syntax casesTarget := atomic(ident " : ")? term
syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic