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

fix: use new sepBy syntax syntax

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-09 13:57:34 +01:00
parent 50c7883b56
commit 7788e75c10
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Notation.lean
View file

@ -199,13 +199,13 @@ syntax[«let!»] "let! " letDecl : tactic
syntax[letrec] withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
syntax inductionAlt := (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
syntax inductionAlts := "with " withPosition("| " sepBy1(inductionAlt, colGe "| "))
syntax inductionAlts := "with " withPosition("| " sepBy1(inductionAlt, "| ", colGe "| "))
syntax[induction] "induction " sepBy1(term, ", ") (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic
syntax casesTarget := atomic(ident " : ")? term
syntax[cases] "cases " sepBy1(casesTarget, ", ") (" using " ident)? (inductionAlts)? : tactic
syntax matchAlt := sepBy1(term, ", ") " => " (hole <|> syntheticHole <|> tacticSeq)
syntax matchAlts := withPosition("| " sepBy1(matchAlt, colGe "| "))
syntax matchAlts := withPosition("| " sepBy1(matchAlt, "| ", colGe "| "))
syntax[«match»] "match " sepBy1(matchDiscr, ", ") (" : " term)? " with " matchAlts : tactic
syntax[introMatch] "intro " matchAlts : tactic