diff --git a/tests/lean/appParserIssue.lean b/tests/lean/appParserIssue.lean index 13b145d7ee..a7f7a759a7 100644 --- a/tests/lean/appParserIssue.lean +++ b/tests/lean/appParserIssue.lean @@ -2,7 +2,7 @@ def f (x : Nat) (g : Nat → Nat) := g x new_frontend -#check f 1 fun x => x -- should fail +#check f 1 fun x => x -- should work #check f 1 (fun x => x) -- should work #check f 1 $ fun x => x -- should work @@ -10,4 +10,4 @@ syntax "foo" term:max term:max : term macro_rules `(foo $x $y) => `(f $x $y) #check foo 1 (fun x => x) -- should work -#check foo 1 fun x => x -- should fail? +#check foo 1 fun x => x -- should work diff --git a/tests/lean/appParserIssue.lean.expected.out b/tests/lean/appParserIssue.lean.expected.out index 2b1320d316..5159445430 100644 --- a/tests/lean/appParserIssue.lean.expected.out +++ b/tests/lean/appParserIssue.lean.expected.out @@ -1,6 +1,5 @@ -f 1 : (Nat → Nat) → Nat -appParserIssue.lean:5:11: error: expected command f 1 (λ (x : Nat), x) : Nat f 1 (λ (x : Nat), x) : Nat f 1 (λ (x : Nat), x) : Nat -appParserIssue.lean:13:13: error: unexpected token at this precedence level; consider parenthesizing the term +f 1 (λ (x : Nat), x) : Nat +f 1 (λ (x : Nat), x) : Nat diff --git a/tests/lean/precissues.lean b/tests/lean/precissues.lean index 26b2127b7a..4cc4bbc3e6 100644 --- a/tests/lean/precissues.lean +++ b/tests/lean/precissues.lean @@ -1,6 +1,6 @@ new_frontend -#check id fun x => x -- should fail +#check id fun x => x -- should work #check 0 diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out index 54fc46896f..9a1e09264a 100644 --- a/tests/lean/precissues.lean.expected.out +++ b/tests/lean/precissues.lean.expected.out @@ -1,8 +1,6 @@ -id : ?m_1 → ?m_1 -precissues.lean:3:10: error: expected command +id (λ (x : ?m_1), x) : ?m_1 → ?m_1 0 : Nat -f 1 : (Nat → Nat) → Nat -precissues.lean:9:11: error: expected command +f 1 (λ (x : Nat), x) : Nat 0 : Nat f 1 (λ (x : Nat), x) : Nat id : ?m_1 → ?m_1