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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2021-10-03 17:20:16 -07:00
parent 7ff013a3a2
commit a12ade3da4
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -8,8 +8,8 @@ StxQuot.lean:8:12: error: expected command, identifier or term
"(«term_+_» (numLit \"1\") \"+\" (numLit \"1\"))"
StxQuot.lean:18:15: error: expected term
"(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\") [])\n []\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\") [])\n []\n []))\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\") [])\n []\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\") [])\n []\n []\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\") [])\n []\n []\n []))\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\") [])\n []\n []\n []))]"
"`Nat.one._@.UnhygienicMain._hyg.1"
"`Nat.one._@.UnhygienicMain._hyg.1"
"(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
@ -18,8 +18,8 @@ StxQuot.lean:18:15: error: expected term
"(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
"(«term_+_» (numLit \"2\") \"+\" (numLit \"1\"))"
"(«term_+_» («term_+_» (numLit \"1\") \"+\" (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\") [])\n []\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\") [])\n []\n []))\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\") [])\n []\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\") [])\n []\n []\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\") [])\n []\n []\n []))\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\") [])\n []\n []\n []))]"
"0"
0
1