From 963063dfeed28bea285965aa7629335b84549f1e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Dec 2019 14:50:14 -0800 Subject: [PATCH] chore: disable tests for type class resolution prototype --- tests/elabissues/typeclass_nested_validate.lean | 1 + tests/lean/fail/typeclass_outparam.lean | 4 ---- tests/lean/run/typeclass_append.lean | 1 + tests/lean/run/typeclass_coerce.lean | 1 + tests/lean/run/typeclass_diamond.lean | 2 ++ tests/lean/run/typeclass_metas_internal_goals.lean | 2 ++ tests/lean/run/typeclass_outparam.lean | 2 ++ 7 files changed, 9 insertions(+), 4 deletions(-) delete mode 100644 tests/lean/fail/typeclass_outparam.lean diff --git a/tests/elabissues/typeclass_nested_validate.lean b/tests/elabissues/typeclass_nested_validate.lean index d6539abda1..3005ce077a 100644 --- a/tests/elabissues/typeclass_nested_validate.lean +++ b/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) diff --git a/tests/lean/fail/typeclass_outparam.lean b/tests/lean/fail/typeclass_outparam.lean deleted file mode 100644 index 7282657202..0000000000 --- a/tests/lean/fail/typeclass_outparam.lean +++ /dev/null @@ -1,4 +0,0 @@ -class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ()) -instance op₁ : OPClass Nat Nat := {} - -#synth OPClass Bool Nat diff --git a/tests/lean/run/typeclass_append.lean b/tests/lean/run/typeclass_append.lean index f4c526198c..32a0c8814a 100644 --- a/tests/lean/run/typeclass_append.lean +++ b/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 := ()) diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean index 58e6565966..4c669381dc 100644 --- a/tests/lean/run/typeclass_coerce.lean +++ b/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) diff --git a/tests/lean/run/typeclass_diamond.lean b/tests/lean/run/typeclass_diamond.lean index c42238917d..80b4eac0e4 100644 --- a/tests/lean/run/typeclass_diamond.lean +++ 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 := ()) diff --git a/tests/lean/run/typeclass_metas_internal_goals.lean b/tests/lean/run/typeclass_metas_internal_goals.lean index e06dd27ea0..f6713d80a8 100644 --- a/tests/lean/run/typeclass_metas_internal_goals.lean +++ b/tests/lean/run/typeclass_metas_internal_goals.lean @@ -1,3 +1,5 @@ +#exit + namespace T1 class Foo (α : Type) : Type := (u : Unit := ()) diff --git a/tests/lean/run/typeclass_outparam.lean b/tests/lean/run/typeclass_outparam.lean index d05569c281..c0bd1ae72c 100644 --- a/tests/lean/run/typeclass_outparam.lean +++ b/tests/lean/run/typeclass_outparam.lean @@ -1,3 +1,5 @@ +#exit + class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ()) instance op₁ : OPClass Nat Nat := {}