diff --git a/test/bench/Basic.lean.leanInk.expected b/test/bench/Basic.lean.leanInk.expected
index d446e2d..de32329 100644
--- a/test/bench/Basic.lean.leanInk.expected
+++ b/test/bench/Basic.lean.leanInk.expected
@@ -980,7 +980,7 @@
     "The `simp` tactic uses lemmas and hypotheses to simplify the main goal target or\nnon-dependent hypotheses. It has many variants:\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n- `simp [h₁, h₂, ..., hₙ]` simplifies the main goal target using the lemmas tagged\n  with the attribute `[simp]` and the given `hᵢ`'s, where the `hᵢ`'s are expressions.\n  If an `hᵢ` is a defined constant `f`, then the equational lemmas associated with\n  `f` are used. This provides a convenient way to unfold `f`.\n- `simp [*]` simplifies the main goal target using the lemmas tagged with the\n  attribute `[simp]` and all hypotheses.\n- `simp only [h₁, h₂, ..., hₙ]` is like `simp [h₁, h₂, ..., hₙ]` but does not use `[simp]` lemmas.\n- `simp [-id₁, ..., -idₙ]` simplifies the main goal target using the lemmas tagged\n  with the attribute `[simp]`, but removes the ones named `idᵢ`.\n- `simp at h₁ h₂ ... hₙ` simplifies the hypotheses `h₁ : T₁` ... `hₙ : Tₙ`. If\n  the target or another hypothesis depends on `hᵢ`, a new simplified hypothesis\n  `hᵢ` is introduced, but the old one remains in the local context.\n- `simp at *` simplifies all the hypotheses and the target.\n- `simp [*] at *` simplifies target and all (propositional) hypotheses using the\n  other hypotheses.\n",
     "_type": "token"},
    {"typeinfo":
-    {"type": "{α : Type ?u.3298} → [self : BEq α] → α → α → Bool",
+    {"type": "{α : Type ?u.2394} → [self : BEq α] → α → α → Bool",
      "name": "BEq.beq",
      "_type": "typeinfo"},
     "semanticType": null,
diff --git a/test/playground/infoTree.lean.leanInk.expected b/test/playground/infoTree.lean.leanInk.expected
index 5f80e26..7170d97 100644
--- a/test/playground/infoTree.lean.leanInk.expected
+++ b/test/playground/infoTree.lean.leanInk.expected
@@ -926,7 +926,7 @@
     "raw": "Array",
     "link": null,
     "docstring":
-    "`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)\nwith elements from `α`. This type has special support in the runtime.\n\nAn array has a size and a capacity; the size is `Array.size` but the capacity\nis not observable from lean code. Arrays perform best when unshared; as long\nas they are used \"linearly\" all updates will be performed destructively on the\narray, so it has comparable performance to mutable arrays in imperative\nprogramming languages.\n",
+    "`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)\nwith elements from `α`. This type has special support in the runtime.\n\nAn array has a size and a capacity; the size is `Array.size` but the capacity\nis not observable from lean code. Arrays perform best when unshared; as long\nas they are used \"linearly\" all updates will be performed destructively on the\narray, so it has comparable performance to mutable arrays in imperative\nprogramming languages.\n\nFrom the point of view of proofs `Array α` is just a wrapper around `List α`.\n",
     "_type": "token"},
    {"typeinfo": null,
     "semanticType": null,
@@ -939,7 +939,7 @@
     "raw": "Array",
     "link": null,
     "docstring":
-    "`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)\nwith elements from `α`. This type has special support in the runtime.\n\nAn array has a size and a capacity; the size is `Array.size` but the capacity\nis not observable from lean code. Arrays perform best when unshared; as long\nas they are used \"linearly\" all updates will be performed destructively on the\narray, so it has comparable performance to mutable arrays in imperative\nprogramming languages.\n",
+    "`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)\nwith elements from `α`. This type has special support in the runtime.\n\nAn array has a size and a capacity; the size is `Array.size` but the capacity\nis not observable from lean code. Arrays perform best when unshared; as long\nas they are used \"linearly\" all updates will be performed destructively on the\narray, so it has comparable performance to mutable arrays in imperative\nprogramming languages.\n\nFrom the point of view of proofs `Array α` is just a wrapper around `List α`.\n",
     "_type": "token"},
    {"typeinfo": null,
     "semanticType": null,
@@ -965,7 +965,7 @@
     "raw": "Array",
     "link": null,
     "docstring":
-    "`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)\nwith elements from `α`. This type has special support in the runtime.\n\nAn array has a size and a capacity; the size is `Array.size` but the capacity\nis not observable from lean code. Arrays perform best when unshared; as long\nas they are used \"linearly\" all updates will be performed destructively on the\narray, so it has comparable performance to mutable arrays in imperative\nprogramming languages.\n",
+    "`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)\nwith elements from `α`. This type has special support in the runtime.\n\nAn array has a size and a capacity; the size is `Array.size` but the capacity\nis not observable from lean code. Arrays perform best when unshared; as long\nas they are used \"linearly\" all updates will be performed destructively on the\narray, so it has comparable performance to mutable arrays in imperative\nprogramming languages.\n\nFrom the point of view of proofs `Array α` is just a wrapper around `List α`.\n",
     "_type": "token"},
    {"typeinfo": null,
     "semanticType": null,