max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-11 19:09:23 -08:00
parent 98608f39b9
commit d30e96bc7d
3 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/StxQuot.lean.expected.out
View file

@ -2,9 +2,9 @@
"<missing>"
"<missing>"
"<missing>"
"(_kind.term._@.Init.Notation._hyg.333 <missing> \"+\" (numLit \"1\"))"
"(_kind.term._@.Init.Notation._hyg.333 <missing> \"+\" (numLit \"1\"))"
"(_kind.term._@.Init.Notation._hyg.333 (numLit \"1\") \"+\" (numLit \"1\"))"
"(_kind.term._@.Init.Notation._hyg.335 <missing> \"+\" (numLit \"1\"))"
"(_kind.term._@.Init.Notation._hyg.335 <missing> \"+\" (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"

4
tests/lean/run/termParserAttr.lean
View file

@ -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 "|]")))

2
tests/lean/syntaxInNamespacesAndPP.lean.expected.out
View file

@ -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))