chore: fix test

2022-03-03 19:15:07 -08:00 · 2022-03-03 19:15:07 -08:00 · b4ddcd600b
commit b4ddcd600b
parent 538eee0b6a
1 changed files with 4 additions and 0 deletions
--- 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,