From fa94ce066056bda6151c25884eac58333ca4f161 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Sep 2021 17:49:03 -0700 Subject: [PATCH] chore: fix test output --- tests/lean/syntaxPrec.lean.expected.out | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out index 4e57125063..48052c3434 100644 --- a/tests/lean/syntaxPrec.lean.expected.out +++ b/tests/lean/syntaxPrec.lean.expected.out @@ -1,3 +1,8 @@ syntaxPrec.lean:1:18: error: expected ':' [Elab.command] syntax "foo"("*" <|> term,+) : term -[Elab.command] failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation) +[Elab.command] @[termParser 1000] +def «termFoo*_» : Lean.ParserDescr✝ := + ParserDescr.node✝ `«termFoo*_» 1022 + (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo") + (ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*") + (ParserDescr.sepBy1✝ (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ") Bool.false✝)))