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.
51 lines
579 B
Plaintext
51 lines
579 B
Plaintext
b 0
|
|
b 1
|
|
b 2
|
|
b 2.5
|
|
n 0
|
|
n 1
|
|
n 2
|
|
n 1.5
|
|
n 2
|
|
n 2.5
|
|
p -1
|
|
p -1
|
|
p 0
|
|
p 1
|
|
p -1
|
|
p -1
|
|
p 1.5
|
|
w 0
|
|
w 1
|
|
w 0
|
|
w 1
|
|
w 0
|
|
w 1.5
|
|
w 0
|
|
w 1.5
|
|
pm 0
|
|
pm 1
|
|
pm 0
|
|
pm 1
|
|
pm 0
|
|
pm 1.5
|
|
pm 0
|
|
pm 1.5
|
|
c 0
|
|
c 1
|
|
c 2
|
|
c 1.5
|
|
c 2
|
|
c 2.5
|
|
{"version": 1,
|
|
"uri": "file:///incrementalInduction.lean",
|
|
"diagnostics":
|
|
[{"source": "Lean 4",
|
|
"severity": 1,
|
|
"range":
|
|
{"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 7}},
|
|
"message":
|
|
"Dependent elimination failed: Failed to solve equation\n n = f n",
|
|
"fullRange":
|
|
{"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 7}}}]}
|