mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
14 lines
450 B
Lean4
14 lines
450 B
Lean4
/-!
|
|
# `rintro` and `intro` error message should point to excess arg
|
|
|
|
Below, the errors should point to `h` because there is no lambda it binds.
|
|
The error should not point to `hn`; it would be OKish to underline the whole line. -/
|
|
|
|
example : (∃ n : Nat, n < 0) → False := by
|
|
rintro ⟨n, hn⟩ h
|
|
--^ collectDiagnostics
|
|
|
|
example : (∃ n : Nat, n < 0) → False := by
|
|
intro ⟨n, hn⟩ h
|
|
--^ collectDiagnostics
|