diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 2e4a2a071e..5b8894c3db 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -1,29 +1,29 @@ -"(Term.id `Nat.one.0 (null))" +"(Term.id `Nat.one._@.UnhygienicMain._hyg.0 (null))" "" "" "" "(Term.add \"+\" (Term.num (numLit \"1\")))" "(Term.add \"+\" (Term.num (numLit \"1\")))" "(Term.add (Term.num (numLit \"1\")) \"+\" (Term.num (numLit \"1\")))" -"(Term.fun \"fun\" (null (Term.id `a.0 (null))) \"=>\" (Term.id `a.0 (null)))" -"(Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))" -"(null\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `bar.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"2\"))))))" -"(Term.id `Nat.one.0 (null))" -"(Term.app (Term.id `f.0 (null)) (null (Term.id `Nat.one.0 (null)) (Term.id `Nat.one.0 (null))))" -"(Term.dollar\n (Term.id `f.0 (null))\n \"$\"\n (Term.app (Term.id `f.0 (null)) (null (Term.id `Nat.one.0 (null)) (Term.num (numLit \"1\")))))" -"(Term.app (Term.id `f.0 (null)) (null (Term.id `Nat.one.0 (null))))" -"(Term.proj (Term.id `Nat.one.0 (null)) \".\" `b.0)" +"(Term.fun \"fun\" (null (Term.id `a._@.UnhygienicMain._hyg.0 (null))) \"=>\" (Term.id `a._@.UnhygienicMain._hyg.0 (null)))" +"(Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))" +"(null\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"2\"))))))" +"(Term.id `Nat.one._@.UnhygienicMain._hyg.0 (null))" +"(Term.app\n (Term.id `f._@.UnhygienicMain._hyg.0 (null))\n (null (Term.id `Nat.one._@.UnhygienicMain._hyg.0 (null)) (Term.id `Nat.one._@.UnhygienicMain._hyg.0 (null))))" +"(Term.dollar\n (Term.id `f._@.UnhygienicMain._hyg.0 (null))\n \"$\"\n (Term.app\n (Term.id `f._@.UnhygienicMain._hyg.0 (null))\n (null (Term.id `Nat.one._@.UnhygienicMain._hyg.0 (null)) (Term.num (numLit \"1\")))))" +"(Term.app (Term.id `f._@.UnhygienicMain._hyg.0 (null)) (null (Term.id `Nat.one._@.UnhygienicMain._hyg.0 (null))))" +"(Term.proj (Term.id `Nat.one._@.UnhygienicMain._hyg.0 (null)) \".\" `b._@.UnhygienicMain._hyg.0)" "(Term.add (Term.num (numLit \"2\")) \"+\" (Term.num (numLit \"1\")))" -"(Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))" -"(null\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `bar.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"2\")))))\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\"))))))" +"(Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))" +"(null\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"2\")))))\n (Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.0 (null))\n (Command.optDeclSig (null) (null))\n (Command.declValSimple \":=\" (Term.num (numLit \"1\"))))))" "0" "1" -"(Term.fun\n \"fun\"\n (null\n (Term.id `a.0 (null))\n (Term.paren \"(\" (null (Term.id `b.0 (null)) (null (Term.typeAscription \":\" (Term.id `Nat.0 (null))))) \")\"))\n \"=>\"\n (Term.num (numLit \"1\")))" -"#[(Term.paren \"(\" (null (Term.id `a.0 (null)) (null (Term.typeAscription \":\" (Term.id `Nat.0 (null))))) \")\"), (Term.id `b.0 (null))]" -"`a.0" -"(Term.forall \"∀\" (null (Term.simpleBinder (null (Term.hole \"_\")))) \",\" (Term.id `c.0 (null)))" +"(Term.fun\n \"fun\"\n (null\n (Term.id `a._@.UnhygienicMain._hyg.0 (null))\n (Term.paren\n \"(\"\n (null\n (Term.id `b._@.UnhygienicMain._hyg.0 (null))\n (null (Term.typeAscription \":\" (Term.id `Nat._@.UnhygienicMain._hyg.0 (null)))))\n \")\"))\n \"=>\"\n (Term.num (numLit \"1\")))" +"#[(Term.paren\n \"(\"\n (null\n (Term.id `a._@.UnhygienicMain._hyg.0 (null))\n (null (Term.typeAscription \":\" (Term.id `Nat._@.UnhygienicMain._hyg.0 (null)))))\n \")\"), (Term.id `b._@.UnhygienicMain._hyg.0 (null))]" +"`a._@.UnhygienicMain._hyg.0" +"(Term.forall \"∀\" (null (Term.simpleBinder (null (Term.hole \"_\")))) \",\" (Term.id `c._@.UnhygienicMain._hyg.0 (null)))" "(Term.simpleBinder (null (Term.hole \"_\")))" -"`a.0" -"(Term.id `a.0 (null (Term.explicitUniv \".{\" (null (Level.num (numLit \"0\"))) \"}\")))" -"#[(Term.matchAlt \"|\" (null (Term.id `a.0 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]" -"#[(Term.matchAlt \"|\" (null (Term.id `a.0 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]" +"`a._@.UnhygienicMain._hyg.0" +"(Term.id `a._@.UnhygienicMain._hyg.0 (null (Term.explicitUniv \".{\" (null (Level.num (numLit \"0\"))) \"}\")))" +"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.0 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]" +"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.0 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]"