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

fix: induction generalizing precedence

Browse source
This commit is contained in:
Mario Carneiro 2022-01-06 23:11:30 -05:00 • committed by Sebastian Ullrich
parent cc4c82a6e7
commit dcaf3c615f
2 changed files with 5 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

@ -394,7 +394,7 @@ macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
syntax inductionAlt := ppDedent(ppLine) "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " term:max+)? (inductionAlts)? : tactic
syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic
syntax generalizeArg := atomic(ident " : ")? term:51 " = " ident
/--

4
tests/lean/run/inductionParse.lean Normal file
View file

@ -0,0 +1,4 @@
example (a b : Nat) : True := by
induction a generalizing b
case zero => trivial
case succ => trivial