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 2020-12-10 11:49:18 -08:00
parent d6c8e48a8e
commit ccabb59e88
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -26,6 +26,6 @@
"`a._@.UnhygienicMain._hyg.1"
"(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(numLit \"0\")] \"}\")"
"#[]"
"(Term.structInst\n \"{\"\n []\n [[(Term.structInstField `a._@.UnhygienicMain._hyg.1 [] \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n []\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
"(Term.structInst\n \"{\"\n []\n [[(Term.structInstField `a._@.UnhygienicMain._hyg.1 [] \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n []\n []\n \"}\")"
"(Term.structInst\n \"{\"\n []\n [[(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n []\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
"(Term.structInst\n \"{\"\n []\n [[(Term.structInstField (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 []) \":=\" `a._@.UnhygienicMain._hyg.1) []]]\n []\n []\n \"}\")"
"(Term.match\n \"match\"\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n []\n \"with\"\n (Term.matchAlts\n []\n [(Term.matchAlt [`a._@.UnhygienicMain._hyg.1] \"=>\" `b._@.UnhygienicMain._hyg.1)\n \"|\"\n (Term.matchAlt\n [(term_+_ `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (term_+_ `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"