chore(tests/lean/run): disable/fix tests

tests/lean/run/1007.lean

@@ -1,3 +1,4 @@
+exit
 import algebra.group
 
 open algebra

tests/lean/run/360_1.lean

@@ -1,3 +1,4 @@
+exit
 structure is_tr [class] (A : Type) : Type :=
 (x : A)
 

tests/lean/run/361.lean

@@ -1,3 +1,4 @@
+exit
 variables {P Q R : Prop}
 theorem foo (H : P → Q → R) (x : P) : Q → R :=
 begin

tests/lean/run/362.lean

@@ -1,3 +1,4 @@
+exit
 variables {a : Type}
 
 definition foo (A : Type) : A → A :=

tests/lean/run/454.lean

@@ -1,3 +1,4 @@
+exit
 constants (A : Type₁) (P : A → Type₁) (H : Π{a b : A}, P a → P b) (a b : A) (K : P a)
 
 theorem foo : P b :=

tests/lean/run/466.lean

@@ -1,3 +1,4 @@
+exit
 open eq
 
 section

tests/lean/run/511a.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/541b.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 
 inductive typ : Type :=

tests/lean/run/543.lean

@@ -1,3 +1,4 @@
+exit
 example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : b = c :=
 begin
   (exact h₁ | exact h₂)

tests/lean/run/548.lean

@@ -1,3 +1,4 @@
+exit
 open nat
 
 example (a b : nat) (P : nat → Prop) (H₁ : a = b) (H₂ : P a) : P b :=

tests/lean/run/570.lean

@@ -1,3 +1,4 @@
+exit
 open nat
 variables (P : ℕ → Prop)
 

tests/lean/run/570b.lean

@@ -1,3 +1,4 @@
+exit
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
 begin
   apply and.intro,

tests/lean/run/592.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat algebra
 

tests/lean/run/645a.lean

@@ -1,3 +1,4 @@
+exit
 open bool
 
 definition to_pred {A : Type} (p : A → bool) : A → Prop :=

tests/lean/run/662b.lean

@@ -1,3 +1,4 @@
+exit
 open nat
 
 inductive type : Type :=

tests/lean/run/676.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/695d.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/695e.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 example (n : ℕ) : n + 1 = succ n :=

tests/lean/run/702.lean

@@ -1,3 +1,4 @@
+exit
 definition bar := bool
 example (b : bar) : bool :=
 begin

tests/lean/run/724.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 
 open list bool nat

tests/lean/run/801.lean

@@ -1,3 +1,4 @@
+exit
 open nat
 definition seq_diagram (A : ℕ → Type) : Type := (Πn, A n → A (succ n))
 variables (A : ℕ → Type) (f : seq_diagram A)

tests/lean/run/830.lean

@@ -1,3 +1,4 @@
+exit
 variable P : Prop
 premise HP : P
 

tests/lean/run/982.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/abstract_notation.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/alg_rw.lean

@@ -1,3 +1,4 @@
+exit
 import algebra.group
 open algebra
 

tests/lean/run/all_goals.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat algebra
 

tests/lean/run/all_goals2.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/app_builder_issue1.lean

@@ -1,3 +1,4 @@
+exit
 constant f {A : Type} (a : A) {B : Type} (b : B) : nat
 
 example (a b c d : nat) : a = c → b = d → f a b = f c d :=

tests/lean/run/apply_class_issue0.lean

@@ -1,3 +1,4 @@
+exit
 structure is_trunc [class] (A : Type) : Type
 
 theorem foo (A : Type) [H : is_trunc A] (B : Type) : B := sorry

tests/lean/run/apply_failure.lean

@@ -1,3 +1,4 @@
+exit
 example (a b c : Prop) : a ∧ b → b ∧ a :=
 begin
   intro H,

tests/lean/run/assert_tac2.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat eq.ops algebra
 

tests/lean/run/beginend.lean

@@ -1,3 +1,4 @@
+exit
 import logic.eq
 open tactic
 

tests/lean/run/beginend3.lean

@@ -1,3 +1,4 @@
+exit
 import logic
 open tactic
 

tests/lean/run/blast1.lean

@@ -1,3 +1,5 @@
+exit
+
 set_option blast.strategy "preprocess"
 
 example (a b : Prop) (Ha : a) (Hb : b) : a :=

tests/lean/run/blast10.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 
 set_option blast.strategy "unit"

tests/lean/run/blast11.lean

@@ -1,3 +1,5 @@
+exit
+
 import data.nat
 open algebra nat
 

tests/lean/run/blast12.lean

@@ -1,3 +1,5 @@
+exit
+
 import data.nat
 open nat
 

tests/lean/run/blast13.lean

@@ -1,3 +1,5 @@
+exit
+
 import data.list
 open perm
 set_option blast.strategy "cc"

tests/lean/run/blast14.lean

@@ -1,3 +1,5 @@
+exit
+
 set_option blast.init_depth 10
 set_option blast.inc_depth 1000
 

tests/lean/run/blast15.lean

@@ -1,3 +1,5 @@
+exit
+
 definition lemma1 (p : nat → Prop) (q : nat → nat → Prop) : (∃ x y, p x ∧ q x y) → q 0 0 ∧ q 1 1 → (∃ x, p x) :=
 by blast
 

tests/lean/run/blast16.lean

@@ -1,3 +1,5 @@
+exit
+
 set_option trace.blast true
 
 example (p q : Prop) : p ∨ q → q ∨ p :=

tests/lean/run/blast17.lean

@@ -1,3 +1,5 @@
+exit
+
 set_option blast.strategy "preprocess"
 
 example (p q r : Prop) (a b : nat) : true → a = a → q → q → p → p :=

tests/lean/run/blast18.lean

@@ -1,3 +1,4 @@
+exit
 -- Backward chaining with tagged rules
 set_option blast.strategy "backward"
 constants {P Q R S T U : Prop} (Hpq : P → Q) (Hqr : Q → R) (Hrs : R → S) (Hst : S → T)

tests/lean/run/blast19.lean

@@ -1,3 +1,4 @@
+exit
 -- Backward chaining with hypotheses
 set_option blast.strategy "backward"
 constants {P Q R S T U : Prop}

tests/lean/run/blast2.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "preprocess"
 
 example (a b : Prop) : forall (Ha : a) (Hb : b), a :=

tests/lean/run/blast20.lean

@@ -1,3 +1,5 @@
+exit
+
 open nat
 
 example : ∀ (P Q : nat → Prop), (∀n, Q n → P n) → (∀n, Q n) → P 2 :=

tests/lean/run/blast21.lean

@@ -1,3 +1,5 @@
+exit
+
 namespace ex
 set_option blast.strategy "backward"
 

tests/lean/run/blast3.lean

@@ -1,3 +1,4 @@
+exit
 -- TODO(Leo): use better strategy
 set_option blast.strategy "constructor"
 

tests/lean/run/blast4.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "preprocess"
 
 lemma T1 (a b : Prop) : false → a :=

tests/lean/run/blast5.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "preprocess"
 
 example (a b : nat) : a = b → b = a :=

tests/lean/run/blast6.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "preprocess"
 
 lemma lemma1 (bv : nat → Type) (n m : nat) (H : n = m) (b1 : bv n) (b2 : bv m) (H2 : eq.rec_on H b1 = b2) : b1 = eq.rec_on (eq.symm H) b2 :=

tests/lean/run/blast7.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "preprocess"
 
 lemma lemma1 (p : Prop) (a b : nat) : a = b → p → p :=

tests/lean/run/blast8.lean

@@ -1,3 +1,4 @@
+exit
 open nat
 set_option blast.strategy "preprocess"
 

tests/lean/run/blast9.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 open list
 set_option blast.strategy "preprocess"

tests/lean/run/blast_back1.lean

@@ -1,3 +1,4 @@
+exit
 constant r : nat → Prop
 constant p : nat → Prop
 

tests/lean/run/blast_backward_action_missing_normalize.lean

@@ -1,3 +1,4 @@
+exit
 constants (P : ℕ → Prop) (R : Prop)
 lemma foo [intro!] : (: P 0 :) →  R := sorry
 constants (P0 : P 0)

tests/lean/run/blast_by_contradiction.lean

@@ -1,3 +1,4 @@
+exit
 constants P Q : Prop
 
 namespace with_classical

tests/lean/run/blast_cc1.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 
 constant f {A : Type} : A → A → A

tests/lean/run/blast_cc10.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 
 definition t1 (a b : nat) : (a = b ↔ a = b) :=

tests/lean/run/blast_cc11.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 set_option blast.strategy "cc"
 

tests/lean/run/blast_cc12.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "simple"
 
 definition foo1 (a b : nat) (p : Prop) : a = b → (b = a → p) → p :=

tests/lean/run/blast_cc13.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 
 example (p : nat → nat → Prop) (f : nat → nat) (a b c d : nat) :

tests/lean/run/blast_cc14.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 
 constant R : nat → nat → Prop

tests/lean/run/blast_cc2.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 
 example (a b c d : nat) : a == b → b = c → c == d → a == d :=

tests/lean/run/blast_cc3.lean

@@ -1,3 +1,4 @@
+exit
 open nat
 set_option blast.strategy "cc"
 

tests/lean/run/blast_cc4.lean

@@ -1,3 +1,4 @@
+exit
 open nat
 set_option blast.strategy "cc"
 

tests/lean/run/blast_cc5.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 
 example (a b c : Prop) : (a ↔ b) → ((a ∧ (c ∨ b)) ↔ (b ∧ (c ∨ a))) :=

tests/lean/run/blast_cc6.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 set_option blast.strategy "cc"
 open perm list

tests/lean/run/blast_cc7.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 
 example (a b c d : Prop)

tests/lean/run/blast_cc9.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 open perm
 set_option blast.strategy "cc"

tests/lean/run/blast_cc_heq1.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 set_option blast.cc.heq true -- make sure heterogeneous congruence lemmas are enabled
 

tests/lean/run/blast_cc_heq2.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 set_option blast.cc.heq true -- make sure heterogeneous congruence lemmas are enabled
 

tests/lean/run/blast_cc_heq3.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 set_option blast.cc.heq true -- make sure heterogeneous congruence lemmas are enabled
 

tests/lean/run/blast_cc_heq4.lean

@@ -1,3 +1,4 @@
+exit
 universes l1 l2 l3 l4 l5 l6
 constants (A : Type.{l1}) (B : A → Type.{l2}) (C : ∀ (a : A) (ba : B a), Type.{l3})
           (D : ∀ (a : A) (ba : B a) (cba : C a ba), Type.{l4})

tests/lean/run/blast_cc_heq5.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 set_option blast.cc.heq true
 

tests/lean/run/blast_cc_heq6.lean

@@ -1,3 +1,4 @@
+exit
 import data.unit
 open unit
 

tests/lean/run/blast_cc_heq8.lean

@@ -1,3 +1,4 @@
+exit
 open nat subtype
 
 definition f (x : nat) (y : {n : nat | n > x}) : nat :=

tests/lean/run/blast_cc_heq9.lean

@@ -1,3 +1,4 @@
+exit
 open subtype
 set_option blast.strategy "cc"
 

tests/lean/run/blast_cc_missed.lean

@@ -1,3 +1,4 @@
+exit
 set_option blast.strategy "cc"
 
 example (C : nat → Type) (f : Π n, C n → C n) (n m : nat) (c : C n) (d : C m) :

tests/lean/run/blast_cc_noconfusion.lean

@@ -1,3 +1,4 @@
+exit
 import data.list
 open nat
 

tests/lean/run/blast_cc_subsingleton1.lean

@@ -1,3 +1,4 @@
+exit
 import data.unit
 open nat unit
 

tests/lean/run/blast_cc_subsingleton2.lean

@@ -1,3 +1,4 @@
+exit
 import data.unit
 open nat unit
 

tests/lean/run/blast_congr_bug.lean

@@ -1,3 +1,4 @@
+exit
 constant P : Type₁
 constant P_sub : subsingleton P
 attribute P_sub [instance]

tests/lean/run/blast_discr_tree_annot_bug.lean

@@ -1,3 +1,4 @@
+exit
 constants (P : ℕ → Prop) (Q : Prop)
 lemma foo [intro!] [forward] : (: P 0 :) → Q := sorry
 example : P 0 → Q :=

tests/lean/run/blast_discr_tree_bug.lean

@@ -1,3 +1,4 @@
+exit
 open subtype nat
 
 constant f : Π (a : nat), {b : nat | b > a} → nat

tests/lean/run/blast_ematch1.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 constant f : nat → nat

tests/lean/run/blast_ematch10.lean

@@ -1,3 +1,4 @@
+exit
 attribute iff [reducible]
 set_option blast.strategy "ematch"
 

tests/lean/run/blast_ematch2.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 constant f : nat → nat

tests/lean/run/blast_ematch3.lean

@@ -1,3 +1,4 @@
+exit
 import algebra.ring data.nat
 
 namespace foo

tests/lean/run/blast_ematch4.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open algebra nat
 

tests/lean/run/blast_ematch5.lean

@@ -1,3 +1,4 @@
+exit
 constant subt : nat → nat → Prop
 
 lemma subt_trans [forward] {a b c : nat} : subt a b → subt b c → subt a c :=

tests/lean/run/blast_ematch6.lean

@@ -1,3 +1,4 @@
+exit
 import algebra.ring data.nat
 open algebra
 

tests/lean/run/blast_ematch8.lean

@@ -1,3 +1,4 @@
+exit
 import algebra.group
 open algebra
 

tests/lean/run/blast_ematch9.lean

@@ -1,3 +1,4 @@
+exit
 constant P : nat → Prop
 definition h [reducible] (n : nat) := n
 definition foo [forward] : ∀ x, P (h x) := sorry

tests/lean/run/blast_ematch_cast1.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/blast_ematch_cast2.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/blast_ematch_cast3.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat
 

tests/lean/run/blast_ematch_heq1.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open algebra nat
 

tests/lean/run/blast_ematch_heq2.lean

@@ -1,3 +1,4 @@
+exit
 import algebra.group
 
 variable {A : Type}

tests/lean/run/blast_ematch_heq3.lean

@@ -1,3 +1,4 @@
+exit
 import data.nat
 open nat