From dfa5cf9282a32c4c968f2fd0847c2c8ad3f9fed8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Mar 2021 12:03:54 -0800 Subject: [PATCH] chore: add optional preprocessing tactic --- src/Init/Notation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index dad55a663c..bbad44f5a6 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -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