From b4ddcd600b2b9c494beba47ca0e6681dd4ca71f7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Mar 2022 19:15:07 -0800
Subject: [PATCH] chore: fix test

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

diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out
index 277babe388..bde72f33e9 100644
--- a/tests/lean/interactive/533.lean.expected.out
+++ b/tests/lean/interactive/533.lean.expected.out
@@ -11,6 +11,10 @@
    "kind": 7,
    "detail":
    "(Type u₁ → Type u₂) → Type u → outParam (Type v) → Type (max (max (max u (u₁ + 1)) u₂) v)"},
+  {"label": "ForIn'",
+   "kind": 7,
+   "detail":
+   "(Type u₁ → Type u₂) →\n  (ρ : Type u) → (α : outParam (Type v)) → [d : outParam (Membership α ρ)] → Type (max (max (max u (u₁ + 1)) u₂) v)"},
   {"label": "ForInStep", "kind": 22, "detail": "Type u → Type u"},
   {"label": "ForM",
    "kind": 7,