max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: update 533 test to include docstring

Browse source
This commit is contained in:
E.W.Ayers 2022-07-20 12:02:46 +01:00 • committed by Leonardo de Moura
parent caa2d9d80f
commit 5bf5abe84f
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/interactive/533.lean.expected.out
View file

@ -2,7 +2,13 @@
"position": {"line": 2, "character": 10}}
{"items":
[{"label": "False", "kind": 22, "detail": "Prop"},
{"label": "Fin", "kind": 22, "detail": "Nat → Type"},
{"label": "Fin",
"kind": 22,
"documentation":
{"value":
"`Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`. ",
"kind": "markdown"},
"detail": "Nat → Type"},
{"label": "Float", "kind": 22, "detail": "Type"},
{"label": "FloatArray", "kind": 22, "detail": "Type"},
{"label": "FloatSpec", "kind": 22, "detail": "Type 1"},