5f119cb54f
Not sure whether it helps or creates more confusion. Note that we are still using the `?` prefix for metavariables on the InfoView and hover info.
14 lines
576 B
Text
14 lines
576 B
Text
{"textDocument": {"uri": "file://completion7.lean"},
|
|
"position": {"line": 0, "character": 10}}
|
|
{"items":
|
|
[{"label": "And", "detail": "Prop → Prop → Prop"},
|
|
{"label": "AndOp", "detail": "Type u → Type u"},
|
|
{"label": "AndThen", "detail": "Type u → Type u"}],
|
|
"isIncomplete": true}
|
|
{"textDocument": {"uri": "file://completion7.lean"},
|
|
"position": {"line": 2, "character": 11}}
|
|
{"items":
|
|
[{"label": "intro", "detail": "a → b → a ∧ b"},
|
|
{"label": "left", "detail": "a ∧ b → a"},
|
|
{"label": "right", "detail": "a ∧ b → b"}],
|
|
"isIncomplete": true}
|