diff --git a/tests/lean/auto_quote_error2.lean b/tests/lean/auto_quote_error2.lean index 1e9cd714ea..47f2832654 100644 --- a/tests/lean/auto_quote_error2.lean +++ b/tests/lean/auto_quote_error2.lean @@ -45,3 +45,11 @@ begin { subst h1 }, --^ error should be at `}` end + +example : true := +begin + { + note h' := eq.refl _, + --^ error should be on this line + } +end \ No newline at end of file diff --git a/tests/lean/auto_quote_error2.lean.expected.out b/tests/lean/auto_quote_error2.lean.expected.out index 153140b3f5..64fce7670a 100644 --- a/tests/lean/auto_quote_error2.lean.expected.out +++ b/tests/lean/auto_quote_error2.lean.expected.out @@ -42,3 +42,8 @@ state: b : ℕ, h2 : b = 0 ⊢ 0 = b +auto_quote_error2.lean:52:15: error: don't know how to synthesize placeholder +context: +⊢ Sort ? +state: +⊢ true