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-04 16:21:12 -08:00
parent 54723409c3
commit 8dbbe37d38
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2,18 +2,18 @@
"<missing>"
"<missing>"
"<missing>"
"(_kind.term._@.Init.Notation._hyg.637 <missing> \"+\" (numLit \"1\"))"
"(_kind.term._@.Init.Notation._hyg.637 <missing> \"+\" (numLit \"1\"))"
"(_kind.term._@.Init.Notation._hyg.637 (numLit \"1\") \"+\" (numLit \"1\"))"
"(termKind._@.Init.Notation._hyg.617 <missing> \"+\" (numLit \"1\"))"
"(termKind._@.Init.Notation._hyg.617 <missing> \"+\" (numLit \"1\"))"
"(termKind._@.Init.Notation._hyg.617 (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\") [])))]"
"`Nat.one._@.UnhygienicMain._hyg.1"
"(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
"(_kind.term._@.Init.Notation._hyg.12477\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (numLit \"1\")]))"
"(termKind._@.Init.Notation._hyg.12077\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.637 (numLit \"2\") \"+\" (numLit \"1\"))"
"(termKind._@.Init.Notation._hyg.617 (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"
@ -28,4 +28,4 @@
"#[]"
"(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.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 [(_kind.term._@.Init.Notation._hyg.637 `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (_kind.term._@.Init.Notation._hyg.637 `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"
"(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 [(termKind._@.Init.Notation._hyg.617 `a._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\"))]\n \"=>\"\n (termKind._@.Init.Notation._hyg.617 `b._@.UnhygienicMain._hyg.1 \"+\" (numLit \"1\")))]))"