From 5bf5abe84f79d8a21740700406e4002fa18c1347 Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Wed, 20 Jul 2022 12:02:46 +0100
Subject: [PATCH] test: update 533 test to include docstring

---
 tests/lean/interactive/533.lean.expected.out | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out
index 9df0a8c394..d7c0ffa2a3 100644
--- a/tests/lean/interactive/533.lean.expected.out
+++ b/tests/lean/interactive/533.lean.expected.out
@@ -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"},