From 89dae7f87785c2cd5df5a7b33301dbfa17d9e875 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Jun 2019 10:33:53 -0700 Subject: [PATCH] fix(library/init/lean/parser/parser): missing result --- library/init/lean/parser/parser.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index ff4febe7e7..2c9b5402eb 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -910,7 +910,7 @@ def trailingParser (tables : ParsingTables) : ParserFn led := partial def trailingLoop (tables : ParsingTables) (rbp : Nat) (c : ParserContext) : Syntax → ParserState → ParserState | left s := let (s, lbp) := currLbp c s in - if rbp ≥ lbp then s + if rbp ≥ lbp then s.pushSyntax left else let s := trailingParser tables left c s in if s.hasError then s