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