chore: disable tests for type class resolution prototype

tests/elabissues/typeclass_nested_validate.lean

@@ -2,6 +2,7 @@
 This example demonstrates a case where Lean4's tabled typeclass resolution may loop.
 It also suggests a workaround, new instance binder semantics, new syntax support, and a new instance validation rule.
 -/
+#exit
 
 class Field (K : Type) := (u : Unit)
 class VectorSpace (K : Type) [Field K] (E : Type) := (u : Unit)

tests/lean/fail/typeclass_outparam.lean

@@ -1,4 +0,0 @@
-class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ())
-instance op₁ : OPClass Nat Nat := {}
-
-#synth OPClass Bool Nat

tests/lean/run/typeclass_append.lean

@@ -5,6 +5,7 @@ Authors: Daniel Selsam
 
 Performance test to ensure quadratic blowup is avoided.
 -/
+#exit
 
 class Append {α : Type} (xs₁ xs₂ : List α) (out : outParam $ List α) : Type :=
 (u : Unit := ())

tests/lean/run/typeclass_coerce.lean

@@ -6,6 +6,7 @@ Authors: Daniel Selsam, Leonardo de Moura
 Declare new, simpler coercion class without the special support for transitivity.
 Test that new tabled typeclass resolution deals with loops and diamonds correctly.
 -/
+#exit
 
 class HasCoerce (a b : Type) :=
 (coerce : a → b)

tests/lean/run/typeclass_diamond.lean

@@ -1,3 +1,5 @@
+#exit
+
 class Top₁   (n : Nat) : Type := (u : Unit := ())
 class Bot₁   (n : Nat) : Type := (u : Unit := ())
 class Left₁  (n : Nat) : Type := (u : Unit := ())

tests/lean/run/typeclass_metas_internal_goals.lean

@@ -1,3 +1,5 @@
+#exit
+
 namespace T1
 
 class Foo (α : Type) : Type := (u : Unit := ())

tests/lean/run/typeclass_outparam.lean

@@ -1,3 +1,5 @@
+#exit
+
 class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ())
 
 instance op₁ : OPClass Nat Nat := {}