diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out index e7cacfc768..165f453f8d 100644 --- a/tests/compiler/termparsertest1.lean.expected.out +++ b/tests/compiler/termparsertest1.lean.expected.out @@ -437,48 +437,46 @@ do pure (a + b) (Term.do "do" - (Term.doSeq - (null - (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null))))) - ";" - (Term.doId - `x - (null (Term.typeSpec ":" (Term.id `Nat (null)))) - "←" - (Term.app (Term.id `f (null)) (null (Term.id `a (null))))) - ";" - (Term.doExpr (Term.app (Term.id `g (null)) (null (Term.id `x (null))))) - ";" - (Term.doLet "let" (Term.letIdDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (null (Term.id `x (null)))))) - ";" - (Term.doPat + (null + (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null))))) + ";" + (Term.doId + `x + (null (Term.typeSpec ":" (Term.id `Nat (null)))) + "←" + (Term.app (Term.id `f (null)) (null (Term.id `a (null))))) + ";" + (Term.doExpr (Term.app (Term.id `g (null)) (null (Term.id `x (null))))) + ";" + (Term.doLet "let" (Term.letIdDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (null (Term.id `x (null)))))) + ";" + (Term.doPat + (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")") + "<-" + (Term.app (Term.id `h (null)) (null (Term.id `x (null)) (Term.id `y (null)))) + (null)) + ";" + (Term.doLet + "let" + (Term.letPatDecl (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")") - "<-" - (Term.app (Term.id `h (null)) (null (Term.id `x (null)) (Term.id `y (null)))) - (null)) - ";" - (Term.doLet - "let" - (Term.letPatDecl - (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")") - (null) - ":=" - (Term.paren "(" (null (Term.id `b (null)) (null (Term.tupleTail "," (null (Term.id `a (null)))))) ")"))) - ";" - (Term.doExpr - (Term.app - (Term.id `pure (null)) - (null (Term.paren "(" (null (Term.add (Term.id `a (null)) "+" (Term.id `b (null))) (null)) ")"))))))) + (null) + ":=" + (Term.paren "(" (null (Term.id `b (null)) (null (Term.tupleTail "," (null (Term.id `a (null)))))) ")"))) + ";" + (Term.doExpr + (Term.app + (Term.id `pure (null)) + (null (Term.paren "(" (null (Term.add (Term.id `a (null)) "+" (Term.id `b (null))) (null)) ")")))))) do { x ← f a; pure $ a + a } (Term.do "do" (Term.bracketedDoSeq "{" - (Term.doSeq - (null - (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null))))) - ";" - (Term.doExpr (Term.dollar (Term.id `pure (null)) "$" (Term.add (Term.id `a (null)) "+" (Term.id `a (null))))))) + (null + (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null))))) + ";" + (Term.doExpr (Term.dollar (Term.id `pure (null)) "$" (Term.add (Term.id `a (null)) "+" (Term.id `a (null)))))) "}")) let f : Nat → Nat → Nat | 0, a => a + 10