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.
31 lines
1.6 KiB
Text
31 lines
1.6 KiB
Text
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 2, "character": 3}}
|
|
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 8, "character": 2}}
|
|
{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
|
|
"goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 13, "character": 3}}
|
|
{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 19, "character": 2}}
|
|
{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
|
|
"goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 24, "character": 3}}
|
|
{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 30, "character": 2}}
|
|
{"rendered": "```lean\ncase succ\nn✝ : Nat\na✝ : True\n⊢ True\n```",
|
|
"goals": ["case succ\nn✝ : Nat\na✝ : True\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 35, "character": 3}}
|
|
{"rendered": "```lean\ncase zero\n⊢ True\n```", "goals": ["case zero\n⊢ True"]}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 41, "character": 2}}
|
|
{"rendered": "no goals", "goals": []}
|
|
{"textDocument": {"uri": "file:///2881.lean"},
|
|
"position": {"line": 46, "character": 4}}
|
|
{"rendered": "```lean\nthis : True\n⊢ True\n```",
|
|
"goals": ["this : True\n⊢ True"]}
|