From f727781792cd8342a2bb31ba3f5810974ae6841c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 May 2018 11:35:08 -0700 Subject: [PATCH] fix(library/init/lean/ir/parser): label --- library/init/lean/ir/parser.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean index 8392096de0..019e0b5167 100644 --- a/library/init/lean/ir/parser.lean +++ b/library/init/lean/ir/parser.lean @@ -164,8 +164,7 @@ def parse_terminator : parser terminator := <|> (keyword "case" >> terminator.case <$> parse_var <*> (symbol "[" >> sep_by1 parse_blockid (symbol ",") <* symbol "]")) def parse_block : parser block := -do id ← parse_blockid, - symbol ":", +do id ← try (parse_blockid <* symbol ":"), ps ← many (parse_phi <* symbol ";"), is ← many (parse_instr <* symbol ";"), t ← parse_terminator <* symbol ";",