From d30e96bc7d608cef53dcadef193301e652062adb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Nov 2020 19:09:23 -0800 Subject: [PATCH] chore: fix tests --- tests/lean/StxQuot.lean.expected.out | 8 ++++---- tests/lean/run/termParserAttr.lean | 4 ++-- tests/lean/syntaxInNamespacesAndPP.lean.expected.out | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 0bdd35aafb..037a4bd787 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -2,9 +2,9 @@ "" "" "" -"(_kind.term._@.Init.Notation._hyg.333 \"+\" (numLit \"1\"))" -"(_kind.term._@.Init.Notation._hyg.333 \"+\" (numLit \"1\"))" -"(_kind.term._@.Init.Notation._hyg.333 (numLit \"1\") \"+\" (numLit \"1\"))" +"(_kind.term._@.Init.Notation._hyg.335 \"+\" (numLit \"1\"))" +"(_kind.term._@.Init.Notation._hyg.335 \"+\" (numLit \"1\"))" +"(_kind.term._@.Init.Notation._hyg.335 (numLit \"1\") \"+\" (numLit \"1\"))" "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1))" "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\"))))" "[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\"))))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"2\"))))]" @@ -13,7 +13,7 @@ "(Term.dollar\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (numLit \"1\")]))" "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1])" "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)" -"(_kind.term._@.Init.Notation._hyg.333 (numLit \"2\") \"+\" (numLit \"1\"))" +"(_kind.term._@.Init.Notation._hyg.335 (numLit \"2\") \"+\" (numLit \"1\"))" "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\"))))" "[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"2\"))))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (numLit \"1\"))))]" "0" diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean index 0a6ea1d13b..ebee6a09e9 100644 --- a/tests/lean/run/termParserAttr.lean +++ b/tests/lean/run/termParserAttr.lean @@ -20,9 +20,9 @@ def tst2 : Parser := symbol "(||" >> termParser >> symbol "||)" @[termParser] def boo : ParserDescr := ParserDescr.node `boo 10 - (ParserDescr.andthen + (ParserDescr.binary `andthen (ParserDescr.symbol "[|") - (ParserDescr.andthen + (ParserDescr.binary `andthen (ParserDescr.cat `term 0) (ParserDescr.symbol "|]"))) diff --git a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out index f07ede733b..a0337457bc 100644 --- a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out +++ b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out @@ -20,5 +20,5 @@ bla true [Elab.command] end def Bla.bla : Lean.ParserDescr := Lean.ParserDescr.node (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Bla") "bla") 1023 - (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol "bla") + (Lean.ParserDescr.binary (Lean.Name.mkStr Lean.Name.anonymous "andthen") (Lean.ParserDescr.symbol "bla") (Lean.ParserDescr.cat (Lean.Name.mkStr Lean.Name.anonymous "term") 0))