diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index 165f453f8d..d8ee793485 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -266,9 +266,11 @@ match x with
(null (Term.id `x (null)))
(null)
"with"
+ (null "|")
(null
- (Term.matchAlt "|" (null (Term.app (Term.id `some (null)) (null (Term.id `x (null))))) "=>" (Term.id `true (null)))
- (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.id `false (null)))))
+ (Term.matchAlt (null (Term.app (Term.id `some (null)) (null (Term.id `x (null))))) "=>" (Term.id `true (null)))
+ "|"
+ (Term.matchAlt (null (Term.id `none (null))) "=>" (Term.id `false (null)))))
match x with
| some y => match y with
@@ -281,9 +283,9 @@ match x with
(null (Term.id `x (null)))
(null)
"with"
+ (null "|")
(null
(Term.matchAlt
- "|"
(null (Term.app (Term.id `some (null)) (null (Term.id `y (null)))))
"=>"
(Term.match
@@ -291,17 +293,19 @@ match x with
(null (Term.id `y (null)))
(null)
"with"
+ (null "|")
(null
(Term.matchAlt
- "|"
(null
(Term.app
(Term.id `some (null))
(null (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")"))))
"=>"
(Term.add (Term.id `a (null)) "+" (Term.id `b (null))))
- (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.num (numLit "1"))))))
- (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.num (numLit "0")))))
+ "|"
+ (Term.matchAlt (null (Term.id `none (null))) "=>" (Term.num (numLit "1"))))))
+ "|"
+ (Term.matchAlt (null (Term.id `none (null))) "=>" (Term.num (numLit "0")))))
Type u
(Term.sortApp (Term.type "Type") (Level.ident `u))
Sort v
@@ -313,19 +317,19 @@ f Type 1
let x := 0; x + 1
(Term.let
"let"
- (Term.letIdDecl `x (null) (null) ":=" (Term.num (numLit "0")))
+ (Term.letDecl `x (null) (null) ":=" (Term.num (numLit "0")))
";"
(Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
let x : Nat := 0; x + 1
(Term.let
"let"
- (Term.letIdDecl `x (null) (null (Term.typeSpec ":" (Term.id `Nat (null)))) ":=" (Term.num (numLit "0")))
+ (Term.letDecl `x (null) (null (Term.typeSpec ":" (Term.id `Nat (null)))) ":=" (Term.num (numLit "0")))
";"
(Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
let f (x : Nat) := x + 1; f 0
(Term.let
"let"
- (Term.letIdDecl
+ (Term.letDecl
`f
(null (Term.explicitBinder "(" (null `x) (null ":" (Term.id `Nat (null))) (null) ")"))
(null)
@@ -336,7 +340,7 @@ let f (x : Nat) := x + 1; f 0
let f {α : Type} (a : α) : α := a; f 10
(Term.let
"let"
- (Term.letIdDecl
+ (Term.letDecl
`f
(null
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}")
@@ -349,7 +353,7 @@ let f {α : Type} (a : α) : α := a; f 10
let f (x) := x + 1; f 10 + f 20
(Term.let
"let"
- (Term.letIdDecl
+ (Term.letDecl
`f
(null (Term.explicitBinder "(" (null `x) (null) (null) ")"))
(null)
@@ -363,9 +367,10 @@ let f (x) := x + 1; f 10 + f 20
let (x, y) := f 10; x + y
(Term.let
"let"
- (Term.letPatDecl
+ (Term.letDecl
(Term.paren "(" (null (Term.id `x (null)) (null (Term.tupleTail "," (null (Term.id `y (null)))))) ")")
(null)
+ (null)
":="
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
";"
@@ -373,13 +378,14 @@ let (x, y) := f 10; x + y
let { fst := x, .. } := f 10; x + x
(Term.let
"let"
- (Term.letPatDecl
+ (Term.letDecl
(Term.structInst
"{"
(null)
(null (Term.structInstField `fst ":=" (Term.id `x (null))) "," (Term.structInstSource ".." (null)))
"}")
(null)
+ (null)
":="
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
";"
@@ -387,15 +393,16 @@ let { fst := x, .. } := f 10; x + x
let x.y := f 10; x
(Term.let
"let"
- (Term.letIdDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
+ (Term.letDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
";"
(Term.id `x (null)))
let x.1 := f 10; x
(Term.let
"let"
- (Term.letPatDecl
+ (Term.letDecl
(Term.proj (Term.id `x (null)) "." (fieldIdx "1"))
(null)
+ (null)
":="
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
";"
@@ -403,9 +410,10 @@ let x.1 := f 10; x
let x[i].y := f 10; x
(Term.let
"let"
- (Term.letPatDecl
+ (Term.letDecl
(Term.proj (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y)
(null)
+ (null)
":="
(Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
";"
@@ -413,9 +421,10 @@ let x[i].y := f 10; x
let x[i] := f 20; x
(Term.let
"let"
- (Term.letPatDecl
+ (Term.letDecl
(Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]")
(null)
+ (null)
":="
(Term.app (Term.id `f (null)) (null (Term.num (numLit "20")))))
";"
@@ -448,7 +457,7 @@ do
";"
(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.doLet "let" (Term.letDecl `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)))))) ")")
@@ -458,9 +467,10 @@ do
";"
(Term.doLet
"let"
- (Term.letPatDecl
+ (Term.letDecl
(Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
(null)
+ (null)
":="
(Term.paren "(" (null (Term.id `b (null)) (null (Term.tupleTail "," (null (Term.id `a (null)))))) ")")))
";"
@@ -484,19 +494,19 @@ let f : Nat → Nat → Nat
f 20
(Term.let
"let"
- (Term.letEqns
+ (Term.letDecl
`f
(null)
(null
(Term.typeSpec ":" (Term.arrow (Term.id `Nat (null)) "→" (Term.arrow (Term.id `Nat (null)) "→" (Term.id `Nat (null))))))
+ "|"
(null
(Term.matchAlt
- "|"
(null (Term.num (numLit "0")) "," (Term.id `a (null)))
"=>"
(Term.add (Term.id `a (null)) "+" (Term.num (numLit "10"))))
+ "|"
(Term.matchAlt
- "|"
(null (Term.add (Term.id `n (null)) "+" (Term.num (numLit "1"))) "," (Term.id `b (null)))
"=>"
(Term.mul (Term.id `n (null)) "*" (Term.id `b (null))))))
@@ -509,6 +519,6 @@ failed as expected, error: :1:10 found '→' as expected, but brackets ar
(x := 20)
failed as expected, error: :1:3 expected ':' or ')'
let x 10; x
-failed as expected, error: :1:8 expected ':='
+failed as expected, error: :1:6 expected '|'
let x := y
failed as expected, error: :1:10 expected ';'
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 669f57dbe3..4dd381b37b 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -25,5 +25,5 @@
"(Term.simpleBinder (null (Term.hole \"_\")))"
"`a._@.UnhygienicMain._hyg.1"
"(Term.id `a._@.UnhygienicMain._hyg.1 (null (Term.explicitUniv \".{\" (null (Level.num (numLit \"0\"))) \"}\")))"
-"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.1 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]"
-"#[(Term.matchAlt \"|\" (null (Term.id `a._@.UnhygienicMain._hyg.1 (null))) \"=>\" (Term.num (numLit \"1\"))), (Term.matchAlt \"|\" (null (Term.hole \"_\")) \"=>\" (Term.num (numLit \"2\")))]"
+"#[]"
+StxQuot.lean:40:74: error: expected '⇒', '=>'