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"},