From fb40b5e80d2606eaf48264648cd90b95af28fef4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Mar 2021 18:07:58 -0800 Subject: [PATCH] chore: fix test --- tests/lean/StxQuot.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index fc2ff6401a..e874e4c768 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -38,7 +38,7 @@ "(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))" "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]" "1" -StxQuot.lean:79:33: error: expected parser to return exactly one syntax object +"(Term.sufficesDecl [] `x._@.UnhygienicMain._hyg.1 (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))" "#[(numLit \"1\"), [(numLit \"2\") (numLit \"3\")], (numLit \"4\")]" "#[(numLit \"2\")]" StxQuot.lean:92:39-92:44: error: unexpected antiquotation splice