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

fix: allow {} as conv

Browse source
This commit is contained in:
Mario Carneiro 2022-08-01 10:42:24 -04:00 • committed by Leonardo de Moura
parent 25aea1b723
commit 5ed3e580ef
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/Conv.lean
View file

@ -13,7 +13,7 @@ namespace Lean.Parser.Tactic.Conv
declare_syntax_cat conv (behavior := both)
syntax convSeq1Indented := withPosition((colGe conv ";"?)+)
syntax convSeqBracketed := "{" (conv ";"?)+ "}"
syntax convSeqBracketed := "{" (conv ";"?)* "}"
-- Order is important: a missing `conv` proof should not be parsed as `{ <missing> }`,
-- automatically closing goals
syntax convSeq := convSeqBracketed <|> convSeq1Indented