8 lines
390 B
Text
8 lines
390 B
Text
{"textDocument": {"uri": "file://plainGoal.lean"},
|
||
"position": {"line": 1, "character": 2}}
|
||
{"rendered": "```lean\nα : Sort ?u\n⊢ α → α\n```",
|
||
"goals": ["α : Sort ?u\n⊢ α → α"]}
|
||
{"textDocument": {"uri": "file://plainGoal.lean"},
|
||
"position": {"line": 1, "character": 3}}
|
||
{"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
|
||
"goals": ["α : Sort ?u\na : α\n⊢ α"]}
|