From f51868240f19e1024f665abbe1daca2a08ae08d8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Jun 2016 16:57:04 -0700 Subject: [PATCH] chore(tests/lean/run): disable/fix tests --- tests/lean/run/1007.lean | 1 + tests/lean/run/360_1.lean | 1 + tests/lean/run/361.lean | 1 + tests/lean/run/362.lean | 1 + tests/lean/run/454.lean | 1 + tests/lean/run/466.lean | 1 + tests/lean/run/511a.lean | 1 + tests/lean/run/541b.lean | 1 + tests/lean/run/543.lean | 1 + tests/lean/run/548.lean | 1 + tests/lean/run/570.lean | 1 + tests/lean/run/570b.lean | 1 + tests/lean/run/592.lean | 1 + tests/lean/run/645a.lean | 1 + tests/lean/run/662b.lean | 1 + tests/lean/run/676.lean | 1 + tests/lean/run/695d.lean | 1 + tests/lean/run/695e.lean | 1 + tests/lean/run/702.lean | 1 + tests/lean/run/724.lean | 1 + tests/lean/run/801.lean | 1 + tests/lean/run/830.lean | 1 + tests/lean/run/982.lean | 1 + tests/lean/run/abstract_notation.lean | 1 + tests/lean/run/alg_rw.lean | 1 + tests/lean/run/all_goals.lean | 1 + tests/lean/run/all_goals2.lean | 1 + tests/lean/run/app_builder_issue1.lean | 1 + tests/lean/run/apply_class_issue0.lean | 1 + tests/lean/run/apply_failure.lean | 1 + tests/lean/run/assert_tac2.lean | 1 + tests/lean/run/beginend.lean | 1 + tests/lean/run/beginend3.lean | 1 + tests/lean/run/blast1.lean | 2 ++ tests/lean/run/blast10.lean | 1 + tests/lean/run/blast11.lean | 2 ++ tests/lean/run/blast12.lean | 2 ++ tests/lean/run/blast13.lean | 2 ++ tests/lean/run/blast14.lean | 2 ++ tests/lean/run/blast15.lean | 2 ++ tests/lean/run/blast16.lean | 2 ++ tests/lean/run/blast17.lean | 2 ++ tests/lean/run/blast18.lean | 1 + tests/lean/run/blast19.lean | 1 + tests/lean/run/blast2.lean | 1 + tests/lean/run/blast20.lean | 2 ++ tests/lean/run/blast21.lean | 2 ++ tests/lean/run/blast3.lean | 1 + tests/lean/run/blast4.lean | 1 + tests/lean/run/blast5.lean | 1 + tests/lean/run/blast6.lean | 1 + tests/lean/run/blast7.lean | 1 + tests/lean/run/blast8.lean | 1 + tests/lean/run/blast9.lean | 1 + tests/lean/run/blast_back1.lean | 1 + ...ast_backward_action_missing_normalize.lean | 1 + tests/lean/run/blast_by_contradiction.lean | 1 + tests/lean/run/blast_cc1.lean | 1 + tests/lean/run/blast_cc10.lean | 1 + tests/lean/run/blast_cc11.lean | 1 + tests/lean/run/blast_cc12.lean | 1 + tests/lean/run/blast_cc13.lean | 1 + tests/lean/run/blast_cc14.lean | 1 + tests/lean/run/blast_cc2.lean | 1 + tests/lean/run/blast_cc3.lean | 1 + tests/lean/run/blast_cc4.lean | 1 + tests/lean/run/blast_cc5.lean | 1 + tests/lean/run/blast_cc6.lean | 1 + tests/lean/run/blast_cc7.lean | 1 + tests/lean/run/blast_cc9.lean | 1 + tests/lean/run/blast_cc_heq1.lean | 1 + tests/lean/run/blast_cc_heq2.lean | 1 + tests/lean/run/blast_cc_heq3.lean | 1 + tests/lean/run/blast_cc_heq4.lean | 1 + tests/lean/run/blast_cc_heq5.lean | 1 + tests/lean/run/blast_cc_heq6.lean | 1 + tests/lean/run/blast_cc_heq8.lean | 1 + tests/lean/run/blast_cc_heq9.lean | 1 + tests/lean/run/blast_cc_missed.lean | 1 + tests/lean/run/blast_cc_noconfusion.lean | 1 + tests/lean/run/blast_cc_subsingleton1.lean | 1 + tests/lean/run/blast_cc_subsingleton2.lean | 1 + tests/lean/run/blast_congr_bug.lean | 1 + .../lean/run/blast_discr_tree_annot_bug.lean | 1 + tests/lean/run/blast_discr_tree_bug.lean | 1 + tests/lean/run/blast_ematch1.lean | 1 + tests/lean/run/blast_ematch10.lean | 1 + tests/lean/run/blast_ematch2.lean | 1 + tests/lean/run/blast_ematch3.lean | 1 + tests/lean/run/blast_ematch4.lean | 1 + tests/lean/run/blast_ematch5.lean | 1 + tests/lean/run/blast_ematch6.lean | 1 + tests/lean/run/blast_ematch8.lean | 1 + tests/lean/run/blast_ematch9.lean | 1 + tests/lean/run/blast_ematch_cast1.lean | 1 + tests/lean/run/blast_ematch_cast2.lean | 1 + tests/lean/run/blast_ematch_cast3.lean | 1 + tests/lean/run/blast_ematch_heq1.lean | 1 + tests/lean/run/blast_ematch_heq2.lean | 1 + tests/lean/run/blast_ematch_heq3.lean | 1 + tests/lean/run/blast_ematch_heq4.lean | 1 + tests/lean/run/blast_ematch_list.lean | 1 + tests/lean/run/blast_ematch_ss1.lean | 1 + tests/lean/run/blast_ematch_sum.lean | 1 + tests/lean/run/blast_ematch_uni_issue.lean | 1 + tests/lean/run/blast_equiv_tests.lean | 1 + tests/lean/run/blast_flat.lean | 1 + tests/lean/run/blast_fun_info_bug.lean | 1 + tests/lean/run/blast_grind1.lean | 1 + tests/lean/run/blast_meta.lean | 1 + tests/lean/run/blast_meta_bug.lean | 1 + tests/lean/run/blast_multiple_nots.lean | 1 + .../lean/run/blast_pattern_inference_bug.lean | 1 + tests/lean/run/blast_rec_eq.lean | 1 + tests/lean/run/blast_recursor1.lean | 1 + tests/lean/run/blast_simp1.lean | 1 + tests/lean/run/blast_simp2.lean | 1 + tests/lean/run/blast_simp3.lean | 1 + tests/lean/run/blast_simp4.lean | 1 + tests/lean/run/blast_simp5.lean | 1 + tests/lean/run/blast_simp_st1.lean | 1 + tests/lean/run/blast_simp_subsingleton.lean | 1 + tests/lean/run/blast_simp_subsingleton2.lean | 1 + tests/lean/run/blast_simp_sum.lean | 1 + tests/lean/run/blast_trace.lean | 1 + tests/lean/run/blast_tuple1.lean | 1 + tests/lean/run/blast_unit.lean | 1 + tests/lean/run/blast_unit_cc.lean | 1 + tests/lean/run/blast_unit_dep.lean | 1 + tests/lean/run/blast_unit_edges.lean | 1 + tests/lean/run/blast_unit_preprocess.lean | 1 + tests/lean/run/blast_vector_test.lean | 1 + tests/lean/run/by_exact.lean | 1 + tests/lean/run/cast_sorry_bug.lean | 10 +++---- tests/lean/run/class4.lean | 1 + tests/lean/run/class7.lean | 1 + tests/lean/run/class8.lean | 1 + tests/lean/run/clear_tac.lean | 1 + tests/lean/run/clears_tac.lean | 1 + tests/lean/run/coe13.lean | 12 ++++---- tests/lean/run/coe14.lean | 1 + tests/lean/run/coe15.lean | 1 + tests/lean/run/coe9.lean | 14 ++++----- tests/lean/run/coercion_bug2.lean | 10 +++---- tests/lean/run/congr_tac.lean | 1 + tests/lean/run/constr_tac.lean | 1 + tests/lean/run/constr_tac2.lean | 1 + tests/lean/run/constr_tac3.lean | 1 + tests/lean/run/constr_tac4.lean | 1 + tests/lean/run/contra1.lean | 1 + tests/lean/run/contra2.lean | 1 + tests/lean/run/def_tac.lean | 1 + tests/lean/run/div2.lean | 1 + tests/lean/run/eassumption.lean | 1 + tests/lean/run/elim.lean | 1 + tests/lean/run/elim2.lean | 1 + tests/lean/run/empty_eq.lean | 10 +++---- tests/lean/run/empty_match_bug.lean | 10 +++---- tests/lean/run/eq14.lean | 1 + tests/lean/run/eq23.lean | 1 + tests/lean/run/eq24.lean | 1 + tests/lean/run/eqn_tac.lean | 1 + tests/lean/run/eqv_tacs.lean | 1 + tests/lean/run/esimp1.lean | 1 + tests/lean/run/exfalso1.lean | 1 + tests/lean/run/export.lean | 4 --- tests/lean/run/fapply.lean | 1 + tests/lean/run/flycheck_blast_cc_heq7.lean | 1 + tests/lean/run/fold.lean | 1 + tests/lean/run/forest.lean | 1 + tests/lean/run/forest2.lean | 1 + tests/lean/run/forest_height.lean | 1 + tests/lean/run/generalizes.lean | 1 + tests/lean/run/goal.lean | 1 + tests/lean/run/group4.lean | 1 + tests/lean/run/group5.lean | 1 + tests/lean/run/have5.lean | 1 + tests/lean/run/iff_rw.lean | 1 + tests/lean/run/imp_curly.lean | 1 + tests/lean/run/ind1.lean | 12 ++++---- tests/lean/run/ind4.lean | 1 + tests/lean/run/ind8.lean | 4 +-- tests/lean/run/ind_tac.lean | 1 + tests/lean/run/induction_tac2.lean | 1 + tests/lean/run/inf_tree.lean | 1 + tests/lean/run/inf_tree2.lean | 1 + tests/lean/run/inf_tree3.lean | 1 + tests/lean/run/intro0.lean | 1 + tests/lean/run/intro_under.lean | 1 + tests/lean/run/intros.lean | 1 + tests/lean/run/inv_bug.lean | 1 + tests/lean/run/inversion1.lean | 1 + tests/lean/run/is_nil.lean | 1 + tests/lean/run/issue332.lean | 1 + tests/lean/run/let_tac.lean | 1 + tests/lean/run/list_elab1.lean | 30 +++++++++---------- tests/lean/run/local_eqns.lean | 1 + tests/lean/run/local_eqns2.lean | 1 + tests/lean/run/match3.lean | 14 ++++----- tests/lean/run/match_tac.lean | 1 + tests/lean/run/match_tac2.lean | 1 + tests/lean/run/match_tac3.lean | 1 + tests/lean/run/match_tac4.lean | 1 + tests/lean/run/mul_zero.lean | 1 + tests/lean/run/nat_bug5.lean | 1 + tests/lean/run/nested_begin.lean | 1 + tests/lean/run/nested_begin_end.lean | 1 + tests/lean/run/nested_rec.lean | 1 + tests/lean/run/new_obtains.lean | 1 + tests/lean/run/new_obtains2.lean | 1 + tests/lean/run/no_confusion_bug.lean | 16 +++++----- tests/lean/run/not_bug1.lean | 6 ++-- tests/lean/run/obtain_tac.lean | 1 + tests/lean/run/opaque_hint_bug.lean | 10 +++---- tests/lean/run/open_fwd_bug.lean | 1 + tests/lean/run/override_on_equations.lean | 20 ++++++------- tests/lean/run/parity.lean | 1 + tests/lean/run/pattern1.lean | 2 ++ tests/lean/run/proof_qed_improved.lean | 1 + tests/lean/run/proof_qed_nested_tac.lean | 2 ++ tests/lean/run/proposition.lean | 1 + tests/lean/run/refine1.lean | 1 + tests/lean/run/refine2.lean | 1 + tests/lean/run/refine3.lean | 1 + tests/lean/run/rename_tac.lean | 1 + tests/lean/run/revert_tac.lean | 1 + tests/lean/run/reverts_tac.lean | 1 + tests/lean/run/rewrite10.lean | 1 + tests/lean/run/rewrite12.lean | 1 + tests/lean/run/rewrite4.lean | 1 + tests/lean/run/rewrite5.lean | 1 + tests/lean/run/rewrite8.lean | 1 + tests/lean/run/rewrite9.lean | 1 + tests/lean/run/rewrite_bug.lean | 1 + tests/lean/run/rewriter1.lean | 1 + tests/lean/run/rewriter11.lean | 1 + tests/lean/run/rewriter12.lean | 1 + tests/lean/run/rewriter13.lean | 1 + tests/lean/run/rewriter14.lean | 1 + tests/lean/run/rewriter15.lean | 1 + tests/lean/run/rewriter16.lean | 1 + tests/lean/run/rewriter17.lean | 1 + tests/lean/run/rewriter18.lean | 1 + tests/lean/run/rewriter2.lean | 1 + tests/lean/run/rewriter3.lean | 1 + tests/lean/run/rw_bug2.lean | 1 + tests/lean/run/rw_set2.lean | 1 + tests/lean/run/scope_bug.lean | 1 + tests/lean/run/secnot.lean | 12 ++++---- tests/lean/run/show2.lean | 6 ++-- tests/lean/run/sigma_no_confusion.lean | 1 + tests/lean/run/simplifier1.lean | 1 + tests/lean/run/soundness.lean | 1 + tests/lean/run/struct_infer.lean | 2 +- tests/lean/run/subst_tact.lean | 1 + tests/lean/run/subst_test.lean | 1 + tests/lean/run/subst_test2.lean | 1 + tests/lean/run/t8.lean | 1 + tests/lean/run/tac1.lean | 1 + tests/lean/run/tactic1.lean | 1 + tests/lean/run/tactic10.lean | 1 + tests/lean/run/tactic11.lean | 1 + tests/lean/run/tactic12.lean | 1 + tests/lean/run/tactic13.lean | 1 + tests/lean/run/tactic15.lean | 1 + tests/lean/run/tactic17.lean | 1 + tests/lean/run/tactic18.lean | 1 + tests/lean/run/tactic19.lean | 1 + tests/lean/run/tactic2.lean | 1 + tests/lean/run/tactic20.lean | 1 + tests/lean/run/tactic21.lean | 1 + tests/lean/run/tactic22.lean | 1 + tests/lean/run/tactic23.lean | 1 + tests/lean/run/tactic24.lean | 1 + tests/lean/run/tactic25.lean | 1 + tests/lean/run/tactic26.lean | 1 + tests/lean/run/tactic27.lean | 1 + tests/lean/run/tactic28.lean | 1 + tests/lean/run/tactic29.lean | 1 + tests/lean/run/tactic3.lean | 1 + tests/lean/run/tactic30.lean | 1 + tests/lean/run/tactic31.lean | 1 + tests/lean/run/tactic4.lean | 1 + tests/lean/run/tactic5.lean | 1 + tests/lean/run/tactic6.lean | 1 + tests/lean/run/tactic7.lean | 1 + tests/lean/run/tactic8.lean | 1 + tests/lean/run/tactic9.lean | 1 + tests/lean/run/tactic_notation.lean | 1 + .../lean/run/tactic_notation_num_arg_bug.lean | 1 + tests/lean/run/tactic_op_overload_bug.lean | 1 + tests/lean/run/tele_eq.lean | 1 + tests/lean/run/tree2.lean | 1 + tests/lean/run/tree3.lean | 2 ++ tests/lean/run/tree_subterm_pred.lean | 1 + tests/lean/run/true_imp_rw.lean | 1 + tests/lean/run/type_equations.lean | 29 ++++++++++-------- tests/lean/run/unfold_tac_bug1.lean | 1 + tests/lean/run/using_bug.lean | 1 + tests/lean/run/using_bug2.lean | 1 + tests/lean/run/using_expr.lean | 1 + tests/lean/run/vars_anywhere.lean | 8 ++--- tests/lean/run/vec_inv.lean | 1 + tests/lean/run/vec_inv2.lean | 1 + tests/lean/run/vec_inv3.lean | 1 + tests/lean/run/vector.lean | 1 + tests/lean/run/vector_subterm_pred.lean | 1 + tests/lean/run/with_attrs1.lean | 1 + 308 files changed, 420 insertions(+), 120 deletions(-) diff --git a/tests/lean/run/1007.lean b/tests/lean/run/1007.lean index 2bf207bed9..9d7dd888bc 100644 --- a/tests/lean/run/1007.lean +++ b/tests/lean/run/1007.lean @@ -1,3 +1,4 @@ +exit import algebra.group open algebra diff --git a/tests/lean/run/360_1.lean b/tests/lean/run/360_1.lean index b039559816..092afd560b 100644 --- a/tests/lean/run/360_1.lean +++ b/tests/lean/run/360_1.lean @@ -1,3 +1,4 @@ +exit structure is_tr [class] (A : Type) : Type := (x : A) diff --git a/tests/lean/run/361.lean b/tests/lean/run/361.lean index 6c09a76704..2cad4f156e 100644 --- a/tests/lean/run/361.lean +++ b/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 diff --git a/tests/lean/run/362.lean b/tests/lean/run/362.lean index c91736dd6f..c3290f7cef 100644 --- a/tests/lean/run/362.lean +++ b/tests/lean/run/362.lean @@ -1,3 +1,4 @@ +exit variables {a : Type} definition foo (A : Type) : A → A := diff --git a/tests/lean/run/454.lean b/tests/lean/run/454.lean index f0ce488b56..7d5b20afb0 100644 --- a/tests/lean/run/454.lean +++ b/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 := diff --git a/tests/lean/run/466.lean b/tests/lean/run/466.lean index c19097265c..c6de1c7103 100644 --- a/tests/lean/run/466.lean +++ b/tests/lean/run/466.lean @@ -1,3 +1,4 @@ +exit open eq section diff --git a/tests/lean/run/511a.lean b/tests/lean/run/511a.lean index 00077163d0..19c58bf3fe 100644 --- a/tests/lean/run/511a.lean +++ b/tests/lean/run/511a.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/541b.lean b/tests/lean/run/541b.lean index 7aeb0c9275..c2e87e8e23 100644 --- a/tests/lean/run/541b.lean +++ b/tests/lean/run/541b.lean @@ -1,3 +1,4 @@ +exit import data.list inductive typ : Type := diff --git a/tests/lean/run/543.lean b/tests/lean/run/543.lean index a47caa5e1e..6d4da28ae0 100644 --- a/tests/lean/run/543.lean +++ b/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₂) diff --git a/tests/lean/run/548.lean b/tests/lean/run/548.lean index 7b0b13e06c..9def56c159 100644 --- a/tests/lean/run/548.lean +++ b/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 := diff --git a/tests/lean/run/570.lean b/tests/lean/run/570.lean index 8bfbb72373..934d259004 100644 --- a/tests/lean/run/570.lean +++ b/tests/lean/run/570.lean @@ -1,3 +1,4 @@ +exit open nat variables (P : ℕ → Prop) diff --git a/tests/lean/run/570b.lean b/tests/lean/run/570b.lean index 7813617889..27ed74b7c3 100644 --- a/tests/lean/run/570b.lean +++ b/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, diff --git a/tests/lean/run/592.lean b/tests/lean/run/592.lean index 1d7d9408bf..e95ae9cdbb 100644 --- a/tests/lean/run/592.lean +++ b/tests/lean/run/592.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra diff --git a/tests/lean/run/645a.lean b/tests/lean/run/645a.lean index d218fbd1ad..3e0894be4e 100644 --- a/tests/lean/run/645a.lean +++ b/tests/lean/run/645a.lean @@ -1,3 +1,4 @@ +exit open bool definition to_pred {A : Type} (p : A → bool) : A → Prop := diff --git a/tests/lean/run/662b.lean b/tests/lean/run/662b.lean index 02621ce8c5..9eb7e7f4da 100644 --- a/tests/lean/run/662b.lean +++ b/tests/lean/run/662b.lean @@ -1,3 +1,4 @@ +exit open nat inductive type : Type := diff --git a/tests/lean/run/676.lean b/tests/lean/run/676.lean index d3e8b2c3fc..1fbdced9cc 100644 --- a/tests/lean/run/676.lean +++ b/tests/lean/run/676.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/695d.lean b/tests/lean/run/695d.lean index 9a12f51ea3..713626e25c 100644 --- a/tests/lean/run/695d.lean +++ b/tests/lean/run/695d.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/695e.lean b/tests/lean/run/695e.lean index 450d76a560..bd36735eb5 100644 --- a/tests/lean/run/695e.lean +++ b/tests/lean/run/695e.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat example (n : ℕ) : n + 1 = succ n := diff --git a/tests/lean/run/702.lean b/tests/lean/run/702.lean index c25b64f3e2..336f82b39f 100644 --- a/tests/lean/run/702.lean +++ b/tests/lean/run/702.lean @@ -1,3 +1,4 @@ +exit definition bar := bool example (b : bar) : bool := begin diff --git a/tests/lean/run/724.lean b/tests/lean/run/724.lean index c5f7495f51..ee07740886 100644 --- a/tests/lean/run/724.lean +++ b/tests/lean/run/724.lean @@ -1,3 +1,4 @@ +exit import data.list open list bool nat diff --git a/tests/lean/run/801.lean b/tests/lean/run/801.lean index 8c86015b8a..e9f48b822e 100644 --- a/tests/lean/run/801.lean +++ b/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) diff --git a/tests/lean/run/830.lean b/tests/lean/run/830.lean index b5aeac8c38..87b5a849c4 100644 --- a/tests/lean/run/830.lean +++ b/tests/lean/run/830.lean @@ -1,3 +1,4 @@ +exit variable P : Prop premise HP : P diff --git a/tests/lean/run/982.lean b/tests/lean/run/982.lean index eac0212c04..f4db8f0fa4 100644 --- a/tests/lean/run/982.lean +++ b/tests/lean/run/982.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/abstract_notation.lean b/tests/lean/run/abstract_notation.lean index 07515d45c8..789ac40326 100644 --- a/tests/lean/run/abstract_notation.lean +++ b/tests/lean/run/abstract_notation.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/alg_rw.lean b/tests/lean/run/alg_rw.lean index a88d36ec35..c3e8e0babf 100644 --- a/tests/lean/run/alg_rw.lean +++ b/tests/lean/run/alg_rw.lean @@ -1,3 +1,4 @@ +exit import algebra.group open algebra diff --git a/tests/lean/run/all_goals.lean b/tests/lean/run/all_goals.lean index 10439fd836..955cdfc923 100644 --- a/tests/lean/run/all_goals.lean +++ b/tests/lean/run/all_goals.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra diff --git a/tests/lean/run/all_goals2.lean b/tests/lean/run/all_goals2.lean index a0a48db868..54608e1531 100644 --- a/tests/lean/run/all_goals2.lean +++ b/tests/lean/run/all_goals2.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/app_builder_issue1.lean b/tests/lean/run/app_builder_issue1.lean index c220cae27c..2a37a7bbdd 100644 --- a/tests/lean/run/app_builder_issue1.lean +++ b/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 := diff --git a/tests/lean/run/apply_class_issue0.lean b/tests/lean/run/apply_class_issue0.lean index 48cb99c4b3..ad2711befa 100644 --- a/tests/lean/run/apply_class_issue0.lean +++ b/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 diff --git a/tests/lean/run/apply_failure.lean b/tests/lean/run/apply_failure.lean index 245bcbeb68..88c36d21ee 100644 --- a/tests/lean/run/apply_failure.lean +++ b/tests/lean/run/apply_failure.lean @@ -1,3 +1,4 @@ +exit example (a b c : Prop) : a ∧ b → b ∧ a := begin intro H, diff --git a/tests/lean/run/assert_tac2.lean b/tests/lean/run/assert_tac2.lean index 9ca6c3257e..1ec202ca60 100644 --- a/tests/lean/run/assert_tac2.lean +++ b/tests/lean/run/assert_tac2.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat eq.ops algebra diff --git a/tests/lean/run/beginend.lean b/tests/lean/run/beginend.lean index 01f1d15d50..5d4611821e 100644 --- a/tests/lean/run/beginend.lean +++ b/tests/lean/run/beginend.lean @@ -1,3 +1,4 @@ +exit import logic.eq open tactic diff --git a/tests/lean/run/beginend3.lean b/tests/lean/run/beginend3.lean index e25e4422a4..2f7324aedc 100644 --- a/tests/lean/run/beginend3.lean +++ b/tests/lean/run/beginend3.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/blast1.lean b/tests/lean/run/blast1.lean index a7acda4fab..d14be931f6 100644 --- a/tests/lean/run/blast1.lean +++ b/tests/lean/run/blast1.lean @@ -1,3 +1,5 @@ +exit + set_option blast.strategy "preprocess" example (a b : Prop) (Ha : a) (Hb : b) : a := diff --git a/tests/lean/run/blast10.lean b/tests/lean/run/blast10.lean index ec0073890f..444e1146bf 100644 --- a/tests/lean/run/blast10.lean +++ b/tests/lean/run/blast10.lean @@ -1,3 +1,4 @@ +exit import data.list set_option blast.strategy "unit" diff --git a/tests/lean/run/blast11.lean b/tests/lean/run/blast11.lean index 08b1da392d..ff3946b529 100644 --- a/tests/lean/run/blast11.lean +++ b/tests/lean/run/blast11.lean @@ -1,3 +1,5 @@ +exit + import data.nat open algebra nat diff --git a/tests/lean/run/blast12.lean b/tests/lean/run/blast12.lean index 56405ebfea..69bacbfd0e 100644 --- a/tests/lean/run/blast12.lean +++ b/tests/lean/run/blast12.lean @@ -1,3 +1,5 @@ +exit + import data.nat open nat diff --git a/tests/lean/run/blast13.lean b/tests/lean/run/blast13.lean index 8d27fffb7c..7f20c7daab 100644 --- a/tests/lean/run/blast13.lean +++ b/tests/lean/run/blast13.lean @@ -1,3 +1,5 @@ +exit + import data.list open perm set_option blast.strategy "cc" diff --git a/tests/lean/run/blast14.lean b/tests/lean/run/blast14.lean index f73fdf78e0..a0f0f06b30 100644 --- a/tests/lean/run/blast14.lean +++ b/tests/lean/run/blast14.lean @@ -1,3 +1,5 @@ +exit + set_option blast.init_depth 10 set_option blast.inc_depth 1000 diff --git a/tests/lean/run/blast15.lean b/tests/lean/run/blast15.lean index 89f704e664..556e10e34c 100644 --- a/tests/lean/run/blast15.lean +++ b/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 diff --git a/tests/lean/run/blast16.lean b/tests/lean/run/blast16.lean index b3bdcb0ca4..b4a9163173 100644 --- a/tests/lean/run/blast16.lean +++ b/tests/lean/run/blast16.lean @@ -1,3 +1,5 @@ +exit + set_option trace.blast true example (p q : Prop) : p ∨ q → q ∨ p := diff --git a/tests/lean/run/blast17.lean b/tests/lean/run/blast17.lean index a36d49e39b..224ea5bb40 100644 --- a/tests/lean/run/blast17.lean +++ b/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 := diff --git a/tests/lean/run/blast18.lean b/tests/lean/run/blast18.lean index 53311c07b3..6c7fadd4d4 100644 --- a/tests/lean/run/blast18.lean +++ b/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) diff --git a/tests/lean/run/blast19.lean b/tests/lean/run/blast19.lean index 32ff2b8a65..41e0db42cb 100644 --- a/tests/lean/run/blast19.lean +++ b/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} diff --git a/tests/lean/run/blast2.lean b/tests/lean/run/blast2.lean index d5dd8c2dae..e8fe2e2ae8 100644 --- a/tests/lean/run/blast2.lean +++ b/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 := diff --git a/tests/lean/run/blast20.lean b/tests/lean/run/blast20.lean index 593ab750f7..e747fb74e3 100644 --- a/tests/lean/run/blast20.lean +++ b/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 := diff --git a/tests/lean/run/blast21.lean b/tests/lean/run/blast21.lean index 1def7095f8..0f3205ec6e 100644 --- a/tests/lean/run/blast21.lean +++ b/tests/lean/run/blast21.lean @@ -1,3 +1,5 @@ +exit + namespace ex set_option blast.strategy "backward" diff --git a/tests/lean/run/blast3.lean b/tests/lean/run/blast3.lean index 72ddcf967f..b7ac9272a8 100644 --- a/tests/lean/run/blast3.lean +++ b/tests/lean/run/blast3.lean @@ -1,3 +1,4 @@ +exit -- TODO(Leo): use better strategy set_option blast.strategy "constructor" diff --git a/tests/lean/run/blast4.lean b/tests/lean/run/blast4.lean index 3d08abde2c..7b4d5cb677 100644 --- a/tests/lean/run/blast4.lean +++ b/tests/lean/run/blast4.lean @@ -1,3 +1,4 @@ +exit set_option blast.strategy "preprocess" lemma T1 (a b : Prop) : false → a := diff --git a/tests/lean/run/blast5.lean b/tests/lean/run/blast5.lean index eda312965f..da827dc274 100644 --- a/tests/lean/run/blast5.lean +++ b/tests/lean/run/blast5.lean @@ -1,3 +1,4 @@ +exit set_option blast.strategy "preprocess" example (a b : nat) : a = b → b = a := diff --git a/tests/lean/run/blast6.lean b/tests/lean/run/blast6.lean index c545005343..c8516c8eb4 100644 --- a/tests/lean/run/blast6.lean +++ b/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 := diff --git a/tests/lean/run/blast7.lean b/tests/lean/run/blast7.lean index dd49488eb3..ff7f0466e5 100644 --- a/tests/lean/run/blast7.lean +++ b/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 := diff --git a/tests/lean/run/blast8.lean b/tests/lean/run/blast8.lean index c7879746f6..c02d3c46b4 100644 --- a/tests/lean/run/blast8.lean +++ b/tests/lean/run/blast8.lean @@ -1,3 +1,4 @@ +exit open nat set_option blast.strategy "preprocess" diff --git a/tests/lean/run/blast9.lean b/tests/lean/run/blast9.lean index ee4e2370b7..5d2ddda510 100644 --- a/tests/lean/run/blast9.lean +++ b/tests/lean/run/blast9.lean @@ -1,3 +1,4 @@ +exit import data.list open list set_option blast.strategy "preprocess" diff --git a/tests/lean/run/blast_back1.lean b/tests/lean/run/blast_back1.lean index 3bd3806992..4d60644a07 100644 --- a/tests/lean/run/blast_back1.lean +++ b/tests/lean/run/blast_back1.lean @@ -1,3 +1,4 @@ +exit constant r : nat → Prop constant p : nat → Prop diff --git a/tests/lean/run/blast_backward_action_missing_normalize.lean b/tests/lean/run/blast_backward_action_missing_normalize.lean index 6343c95ca0..257a0fb53a 100644 --- a/tests/lean/run/blast_backward_action_missing_normalize.lean +++ b/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) diff --git a/tests/lean/run/blast_by_contradiction.lean b/tests/lean/run/blast_by_contradiction.lean index 4eff2381f8..ca7f34db79 100644 --- a/tests/lean/run/blast_by_contradiction.lean +++ b/tests/lean/run/blast_by_contradiction.lean @@ -1,3 +1,4 @@ +exit constants P Q : Prop namespace with_classical diff --git a/tests/lean/run/blast_cc1.lean b/tests/lean/run/blast_cc1.lean index 0abd9f4540..09a8c8182e 100644 --- a/tests/lean/run/blast_cc1.lean +++ b/tests/lean/run/blast_cc1.lean @@ -1,3 +1,4 @@ +exit import data.list constant f {A : Type} : A → A → A diff --git a/tests/lean/run/blast_cc10.lean b/tests/lean/run/blast_cc10.lean index 6fd059d097..e79640f423 100644 --- a/tests/lean/run/blast_cc10.lean +++ b/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) := diff --git a/tests/lean/run/blast_cc11.lean b/tests/lean/run/blast_cc11.lean index 9242952a91..71e860c815 100644 --- a/tests/lean/run/blast_cc11.lean +++ b/tests/lean/run/blast_cc11.lean @@ -1,3 +1,4 @@ +exit import data.list set_option blast.strategy "cc" diff --git a/tests/lean/run/blast_cc12.lean b/tests/lean/run/blast_cc12.lean index f9486afcee..7c4c5b5efa 100644 --- a/tests/lean/run/blast_cc12.lean +++ b/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 := diff --git a/tests/lean/run/blast_cc13.lean b/tests/lean/run/blast_cc13.lean index d8673733a0..f5672d7076 100644 --- a/tests/lean/run/blast_cc13.lean +++ b/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) : diff --git a/tests/lean/run/blast_cc14.lean b/tests/lean/run/blast_cc14.lean index 17d59c7242..5eb38895b5 100644 --- a/tests/lean/run/blast_cc14.lean +++ b/tests/lean/run/blast_cc14.lean @@ -1,3 +1,4 @@ +exit set_option blast.strategy "cc" constant R : nat → nat → Prop diff --git a/tests/lean/run/blast_cc2.lean b/tests/lean/run/blast_cc2.lean index c9d018ffc5..2842ec05af 100644 --- a/tests/lean/run/blast_cc2.lean +++ b/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 := diff --git a/tests/lean/run/blast_cc3.lean b/tests/lean/run/blast_cc3.lean index 9294a4c4aa..e5b1ac1e83 100644 --- a/tests/lean/run/blast_cc3.lean +++ b/tests/lean/run/blast_cc3.lean @@ -1,3 +1,4 @@ +exit open nat set_option blast.strategy "cc" diff --git a/tests/lean/run/blast_cc4.lean b/tests/lean/run/blast_cc4.lean index 1d024b8778..ae7a7b51ec 100644 --- a/tests/lean/run/blast_cc4.lean +++ b/tests/lean/run/blast_cc4.lean @@ -1,3 +1,4 @@ +exit open nat set_option blast.strategy "cc" diff --git a/tests/lean/run/blast_cc5.lean b/tests/lean/run/blast_cc5.lean index 84c24309f5..1541e95150 100644 --- a/tests/lean/run/blast_cc5.lean +++ b/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))) := diff --git a/tests/lean/run/blast_cc6.lean b/tests/lean/run/blast_cc6.lean index 903ef247de..e43f3c8a17 100644 --- a/tests/lean/run/blast_cc6.lean +++ b/tests/lean/run/blast_cc6.lean @@ -1,3 +1,4 @@ +exit import data.list set_option blast.strategy "cc" open perm list diff --git a/tests/lean/run/blast_cc7.lean b/tests/lean/run/blast_cc7.lean index eff36e9004..a94dc84e37 100644 --- a/tests/lean/run/blast_cc7.lean +++ b/tests/lean/run/blast_cc7.lean @@ -1,3 +1,4 @@ +exit set_option blast.strategy "cc" example (a b c d : Prop) diff --git a/tests/lean/run/blast_cc9.lean b/tests/lean/run/blast_cc9.lean index acf4b25bcf..c2a85e36d6 100644 --- a/tests/lean/run/blast_cc9.lean +++ b/tests/lean/run/blast_cc9.lean @@ -1,3 +1,4 @@ +exit import data.list open perm set_option blast.strategy "cc" diff --git a/tests/lean/run/blast_cc_heq1.lean b/tests/lean/run/blast_cc_heq1.lean index c817f76b49..b65331cf19 100644 --- a/tests/lean/run/blast_cc_heq1.lean +++ b/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 diff --git a/tests/lean/run/blast_cc_heq2.lean b/tests/lean/run/blast_cc_heq2.lean index 0bccb9a62e..eb019dc2f0 100644 --- a/tests/lean/run/blast_cc_heq2.lean +++ b/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 diff --git a/tests/lean/run/blast_cc_heq3.lean b/tests/lean/run/blast_cc_heq3.lean index 17569f1db6..930d36c4eb 100644 --- a/tests/lean/run/blast_cc_heq3.lean +++ b/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 diff --git a/tests/lean/run/blast_cc_heq4.lean b/tests/lean/run/blast_cc_heq4.lean index c42325d607..90fa99ee99 100644 --- a/tests/lean/run/blast_cc_heq4.lean +++ b/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}) diff --git a/tests/lean/run/blast_cc_heq5.lean b/tests/lean/run/blast_cc_heq5.lean index 4708833caa..1ac090e7ca 100644 --- a/tests/lean/run/blast_cc_heq5.lean +++ b/tests/lean/run/blast_cc_heq5.lean @@ -1,3 +1,4 @@ +exit set_option blast.strategy "cc" set_option blast.cc.heq true diff --git a/tests/lean/run/blast_cc_heq6.lean b/tests/lean/run/blast_cc_heq6.lean index 94e7d6c741..884802b263 100644 --- a/tests/lean/run/blast_cc_heq6.lean +++ b/tests/lean/run/blast_cc_heq6.lean @@ -1,3 +1,4 @@ +exit import data.unit open unit diff --git a/tests/lean/run/blast_cc_heq8.lean b/tests/lean/run/blast_cc_heq8.lean index a90ad66722..cf7fcd20ec 100644 --- a/tests/lean/run/blast_cc_heq8.lean +++ b/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 := diff --git a/tests/lean/run/blast_cc_heq9.lean b/tests/lean/run/blast_cc_heq9.lean index bf3818592b..c3627d55b6 100644 --- a/tests/lean/run/blast_cc_heq9.lean +++ b/tests/lean/run/blast_cc_heq9.lean @@ -1,3 +1,4 @@ +exit open subtype set_option blast.strategy "cc" diff --git a/tests/lean/run/blast_cc_missed.lean b/tests/lean/run/blast_cc_missed.lean index c91cce5759..fe826178de 100644 --- a/tests/lean/run/blast_cc_missed.lean +++ b/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) : diff --git a/tests/lean/run/blast_cc_noconfusion.lean b/tests/lean/run/blast_cc_noconfusion.lean index 0e8c51c740..3401375f89 100644 --- a/tests/lean/run/blast_cc_noconfusion.lean +++ b/tests/lean/run/blast_cc_noconfusion.lean @@ -1,3 +1,4 @@ +exit import data.list open nat diff --git a/tests/lean/run/blast_cc_subsingleton1.lean b/tests/lean/run/blast_cc_subsingleton1.lean index 663eedb417..020ba1bf96 100644 --- a/tests/lean/run/blast_cc_subsingleton1.lean +++ b/tests/lean/run/blast_cc_subsingleton1.lean @@ -1,3 +1,4 @@ +exit import data.unit open nat unit diff --git a/tests/lean/run/blast_cc_subsingleton2.lean b/tests/lean/run/blast_cc_subsingleton2.lean index fb4f9bb023..bb49969b7a 100644 --- a/tests/lean/run/blast_cc_subsingleton2.lean +++ b/tests/lean/run/blast_cc_subsingleton2.lean @@ -1,3 +1,4 @@ +exit import data.unit open nat unit diff --git a/tests/lean/run/blast_congr_bug.lean b/tests/lean/run/blast_congr_bug.lean index 0604421da1..1961d0522e 100644 --- a/tests/lean/run/blast_congr_bug.lean +++ b/tests/lean/run/blast_congr_bug.lean @@ -1,3 +1,4 @@ +exit constant P : Type₁ constant P_sub : subsingleton P attribute P_sub [instance] diff --git a/tests/lean/run/blast_discr_tree_annot_bug.lean b/tests/lean/run/blast_discr_tree_annot_bug.lean index 734523e907..ab4d8188bb 100644 --- a/tests/lean/run/blast_discr_tree_annot_bug.lean +++ b/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 := diff --git a/tests/lean/run/blast_discr_tree_bug.lean b/tests/lean/run/blast_discr_tree_bug.lean index d7a0b41166..85a1cd6458 100644 --- a/tests/lean/run/blast_discr_tree_bug.lean +++ b/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 diff --git a/tests/lean/run/blast_ematch1.lean b/tests/lean/run/blast_ematch1.lean index 901de7d4e7..46fd99f5c4 100644 --- a/tests/lean/run/blast_ematch1.lean +++ b/tests/lean/run/blast_ematch1.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat constant f : nat → nat diff --git a/tests/lean/run/blast_ematch10.lean b/tests/lean/run/blast_ematch10.lean index 0fa71972ac..73dc1db87d 100644 --- a/tests/lean/run/blast_ematch10.lean +++ b/tests/lean/run/blast_ematch10.lean @@ -1,3 +1,4 @@ +exit attribute iff [reducible] set_option blast.strategy "ematch" diff --git a/tests/lean/run/blast_ematch2.lean b/tests/lean/run/blast_ematch2.lean index 2ca111975b..affa4288f9 100644 --- a/tests/lean/run/blast_ematch2.lean +++ b/tests/lean/run/blast_ematch2.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat constant f : nat → nat diff --git a/tests/lean/run/blast_ematch3.lean b/tests/lean/run/blast_ematch3.lean index 8147b1eee1..2721418397 100644 --- a/tests/lean/run/blast_ematch3.lean +++ b/tests/lean/run/blast_ematch3.lean @@ -1,3 +1,4 @@ +exit import algebra.ring data.nat namespace foo diff --git a/tests/lean/run/blast_ematch4.lean b/tests/lean/run/blast_ematch4.lean index 42d1ab5bfd..80786faed1 100644 --- a/tests/lean/run/blast_ematch4.lean +++ b/tests/lean/run/blast_ematch4.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra nat diff --git a/tests/lean/run/blast_ematch5.lean b/tests/lean/run/blast_ematch5.lean index 5a8e8c45bc..4fb2531bd6 100644 --- a/tests/lean/run/blast_ematch5.lean +++ b/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 := diff --git a/tests/lean/run/blast_ematch6.lean b/tests/lean/run/blast_ematch6.lean index d9bddeaee9..124a974f4f 100644 --- a/tests/lean/run/blast_ematch6.lean +++ b/tests/lean/run/blast_ematch6.lean @@ -1,3 +1,4 @@ +exit import algebra.ring data.nat open algebra diff --git a/tests/lean/run/blast_ematch8.lean b/tests/lean/run/blast_ematch8.lean index 84f2053deb..752c05207b 100644 --- a/tests/lean/run/blast_ematch8.lean +++ b/tests/lean/run/blast_ematch8.lean @@ -1,3 +1,4 @@ +exit import algebra.group open algebra diff --git a/tests/lean/run/blast_ematch9.lean b/tests/lean/run/blast_ematch9.lean index 44963cb84a..86ba7e1461 100644 --- a/tests/lean/run/blast_ematch9.lean +++ b/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 diff --git a/tests/lean/run/blast_ematch_cast1.lean b/tests/lean/run/blast_ematch_cast1.lean index 83c02c3814..5ababe724e 100644 --- a/tests/lean/run/blast_ematch_cast1.lean +++ b/tests/lean/run/blast_ematch_cast1.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/blast_ematch_cast2.lean b/tests/lean/run/blast_ematch_cast2.lean index 1eaf5498d2..8d90a35aaa 100644 --- a/tests/lean/run/blast_ematch_cast2.lean +++ b/tests/lean/run/blast_ematch_cast2.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/blast_ematch_cast3.lean b/tests/lean/run/blast_ematch_cast3.lean index 18af9d2737..1cfd86eacc 100644 --- a/tests/lean/run/blast_ematch_cast3.lean +++ b/tests/lean/run/blast_ematch_cast3.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/blast_ematch_heq1.lean b/tests/lean/run/blast_ematch_heq1.lean index 67df52e1b8..f4d72e6e03 100644 --- a/tests/lean/run/blast_ematch_heq1.lean +++ b/tests/lean/run/blast_ematch_heq1.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra nat diff --git a/tests/lean/run/blast_ematch_heq2.lean b/tests/lean/run/blast_ematch_heq2.lean index 57b6d5dea5..9ca400acd5 100644 --- a/tests/lean/run/blast_ematch_heq2.lean +++ b/tests/lean/run/blast_ematch_heq2.lean @@ -1,3 +1,4 @@ +exit import algebra.group variable {A : Type} diff --git a/tests/lean/run/blast_ematch_heq3.lean b/tests/lean/run/blast_ematch_heq3.lean index 90f78755be..36215473fc 100644 --- a/tests/lean/run/blast_ematch_heq3.lean +++ b/tests/lean/run/blast_ematch_heq3.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/blast_ematch_heq4.lean b/tests/lean/run/blast_ematch_heq4.lean index 5286d2f155..39607cdb89 100644 --- a/tests/lean/run/blast_ematch_heq4.lean +++ b/tests/lean/run/blast_ematch_heq4.lean @@ -1,3 +1,4 @@ +exit universe l constants (A : Type.{l}) (P : A → Prop) (h : Π (a : A), P a → A) (f g : A → A) constants (p : ∀ a, P a) diff --git a/tests/lean/run/blast_ematch_list.lean b/tests/lean/run/blast_ematch_list.lean index a749f364ef..62517f848f 100644 --- a/tests/lean/run/blast_ematch_list.lean +++ b/tests/lean/run/blast_ematch_list.lean @@ -1,3 +1,4 @@ +exit import data.list open list diff --git a/tests/lean/run/blast_ematch_ss1.lean b/tests/lean/run/blast_ematch_ss1.lean index 7bbd923808..2b852385db 100644 --- a/tests/lean/run/blast_ematch_ss1.lean +++ b/tests/lean/run/blast_ematch_ss1.lean @@ -1,3 +1,4 @@ +exit constant q (a : Prop) (h : decidable a) : Prop constant r : nat → Prop constant rdec : ∀ a, decidable (r a) diff --git a/tests/lean/run/blast_ematch_sum.lean b/tests/lean/run/blast_ematch_sum.lean index 649805ffc2..d74091e83b 100644 --- a/tests/lean/run/blast_ematch_sum.lean +++ b/tests/lean/run/blast_ematch_sum.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/blast_ematch_uni_issue.lean b/tests/lean/run/blast_ematch_uni_issue.lean index c70b42686b..4735ea6199 100644 --- a/tests/lean/run/blast_ematch_uni_issue.lean +++ b/tests/lean/run/blast_ematch_uni_issue.lean @@ -1,3 +1,4 @@ +exit set_option blast.ematch true variable {A : Type} definition R : A → A → Prop := sorry diff --git a/tests/lean/run/blast_equiv_tests.lean b/tests/lean/run/blast_equiv_tests.lean index dbee78fa82..bbecee5271 100644 --- a/tests/lean/run/blast_equiv_tests.lean +++ b/tests/lean/run/blast_equiv_tests.lean @@ -1,3 +1,4 @@ +exit import data.sum data.nat open function diff --git a/tests/lean/run/blast_flat.lean b/tests/lean/run/blast_flat.lean index c16b6eea21..9f91c5940e 100644 --- a/tests/lean/run/blast_flat.lean +++ b/tests/lean/run/blast_flat.lean @@ -1,3 +1,4 @@ +exit open nat subtype definition f (x : nat) (y : {n : nat | n > x}) : nat := diff --git a/tests/lean/run/blast_fun_info_bug.lean b/tests/lean/run/blast_fun_info_bug.lean index 1d04e48261..66ed44f257 100644 --- a/tests/lean/run/blast_fun_info_bug.lean +++ b/tests/lean/run/blast_fun_info_bug.lean @@ -1,3 +1,4 @@ +exit definition set (A : Type) := A → Prop set_option blast.strategy "preprocess" diff --git a/tests/lean/run/blast_grind1.lean b/tests/lean/run/blast_grind1.lean index 54fe83b08f..0624d1cc74 100644 --- a/tests/lean/run/blast_grind1.lean +++ b/tests/lean/run/blast_grind1.lean @@ -1,3 +1,4 @@ +exit set_option blast.strategy "core_grind" example (a b c : nat) : a = b ∨ a = c → b = c → b = a := diff --git a/tests/lean/run/blast_meta.lean b/tests/lean/run/blast_meta.lean index be6ccb0b02..973cc062c0 100644 --- a/tests/lean/run/blast_meta.lean +++ b/tests/lean/run/blast_meta.lean @@ -1,3 +1,4 @@ +exit constant p : nat → nat → Prop constant p_trans : ∀ a b c, p a b → p b c → p a c diff --git a/tests/lean/run/blast_meta_bug.lean b/tests/lean/run/blast_meta_bug.lean index 8d2ff385ec..74a4198e35 100644 --- a/tests/lean/run/blast_meta_bug.lean +++ b/tests/lean/run/blast_meta_bug.lean @@ -1,3 +1,4 @@ +exit constants {A : Type.{1}} (P : A → Prop) (Q : A → Prop) definition H [forward] : ∀ a, (: P a :) → Exists Q := sorry diff --git a/tests/lean/run/blast_multiple_nots.lean b/tests/lean/run/blast_multiple_nots.lean index 5ab9b9259f..cf14cb860b 100644 --- a/tests/lean/run/blast_multiple_nots.lean +++ b/tests/lean/run/blast_multiple_nots.lean @@ -1,3 +1,4 @@ +exit constants a b c d : Prop set_option blast.strategy "unit" diff --git a/tests/lean/run/blast_pattern_inference_bug.lean b/tests/lean/run/blast_pattern_inference_bug.lean index af308c0ef1..d76b30d335 100644 --- a/tests/lean/run/blast_pattern_inference_bug.lean +++ b/tests/lean/run/blast_pattern_inference_bug.lean @@ -1,3 +1,4 @@ +exit constant p : nat → Prop constant q : ∀ a, p a → Prop lemma ex [forward] : ∀ (a : nat) (h : p a), (:q a h:) := sorry diff --git a/tests/lean/run/blast_rec_eq.lean b/tests/lean/run/blast_rec_eq.lean index 35354ceb66..4dbf8df1b4 100644 --- a/tests/lean/run/blast_rec_eq.lean +++ b/tests/lean/run/blast_rec_eq.lean @@ -1,3 +1,4 @@ +exit open nat lemma addz [simp] : ∀ a : nat, a + 0 = a := sorry diff --git a/tests/lean/run/blast_recursor1.lean b/tests/lean/run/blast_recursor1.lean index dd5ea80176..98326b24b0 100644 --- a/tests/lean/run/blast_recursor1.lean +++ b/tests/lean/run/blast_recursor1.lean @@ -1,3 +1,4 @@ +exit constants P Q : nat → Prop inductive foo : nat → Prop := | intro1 : ∀ n, P n → foo n diff --git a/tests/lean/run/blast_simp1.lean b/tests/lean/run/blast_simp1.lean index 39fcb27eb8..f955883f45 100644 --- a/tests/lean/run/blast_simp1.lean +++ b/tests/lean/run/blast_simp1.lean @@ -1,3 +1,4 @@ +exit example (a b c : Prop) : a ∧ b ∧ c ↔ c ∧ b ∧ a := by simp diff --git a/tests/lean/run/blast_simp2.lean b/tests/lean/run/blast_simp2.lean index adbd269713..c45d199776 100644 --- a/tests/lean/run/blast_simp2.lean +++ b/tests/lean/run/blast_simp2.lean @@ -1,3 +1,4 @@ +exit definition tst1 (a b : Prop) : a ∧ b ∧ true → b ∧ a := by simp diff --git a/tests/lean/run/blast_simp3.lean b/tests/lean/run/blast_simp3.lean index cbbb6b549e..422360f5ab 100644 --- a/tests/lean/run/blast_simp3.lean +++ b/tests/lean/run/blast_simp3.lean @@ -1,3 +1,4 @@ +exit example (A : Type₁) (a₁ a₂ : A) : a₁ = a₂ → (λ (B : Type₁) (f : A → B), f a₁) = (λ (B : Type₁) (f : A → B), f a₂) := by simp diff --git a/tests/lean/run/blast_simp4.lean b/tests/lean/run/blast_simp4.lean index 0b5d5e89c1..919a550e87 100644 --- a/tests/lean/run/blast_simp4.lean +++ b/tests/lean/run/blast_simp4.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/blast_simp5.lean b/tests/lean/run/blast_simp5.lean index 91821100dc..ba4a521a2c 100644 --- a/tests/lean/run/blast_simp5.lean +++ b/tests/lean/run/blast_simp5.lean @@ -1,3 +1,4 @@ +exit definition f : nat → nat := sorry definition g (a : nat) := f a lemma gax [simp] : ∀ a, g a = 0 := sorry diff --git a/tests/lean/run/blast_simp_st1.lean b/tests/lean/run/blast_simp_st1.lean index 290e3b168f..e0841d7e8e 100644 --- a/tests/lean/run/blast_simp_st1.lean +++ b/tests/lean/run/blast_simp_st1.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra nat diff --git a/tests/lean/run/blast_simp_subsingleton.lean b/tests/lean/run/blast_simp_subsingleton.lean index f6eb70d6b1..57cd0143f5 100644 --- a/tests/lean/run/blast_simp_subsingleton.lean +++ b/tests/lean/run/blast_simp_subsingleton.lean @@ -1,3 +1,4 @@ +exit import data.unit open nat unit diff --git a/tests/lean/run/blast_simp_subsingleton2.lean b/tests/lean/run/blast_simp_subsingleton2.lean index f8fd199462..ea98911750 100644 --- a/tests/lean/run/blast_simp_subsingleton2.lean +++ b/tests/lean/run/blast_simp_subsingleton2.lean @@ -1,3 +1,4 @@ +exit import data.unit open nat unit diff --git a/tests/lean/run/blast_simp_sum.lean b/tests/lean/run/blast_simp_sum.lean index 289e2aa942..b0b884f8ff 100644 --- a/tests/lean/run/blast_simp_sum.lean +++ b/tests/lean/run/blast_simp_sum.lean @@ -1,3 +1,4 @@ +exit import data.nat open - [simp] nat diff --git a/tests/lean/run/blast_trace.lean b/tests/lean/run/blast_trace.lean index 0ffbbe06e1..d4a7c5ad21 100644 --- a/tests/lean/run/blast_trace.lean +++ b/tests/lean/run/blast_trace.lean @@ -1,3 +1,4 @@ +exit set_option trace.blast true set_option trace.blast.action false diff --git a/tests/lean/run/blast_tuple1.lean b/tests/lean/run/blast_tuple1.lean index 129c774428..6ab5f07e77 100644 --- a/tests/lean/run/blast_tuple1.lean +++ b/tests/lean/run/blast_tuple1.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/blast_unit.lean b/tests/lean/run/blast_unit.lean index 3c58c1ad2c..de36aa73d9 100644 --- a/tests/lean/run/blast_unit.lean +++ b/tests/lean/run/blast_unit.lean @@ -1,3 +1,4 @@ +exit -- Testing all possible cases of [unit_action] set_option blast.strategy "unit" variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop} diff --git a/tests/lean/run/blast_unit_cc.lean b/tests/lean/run/blast_unit_cc.lean index 9d7afa02ec..7f199e5e14 100644 --- a/tests/lean/run/blast_unit_cc.lean +++ b/tests/lean/run/blast_unit_cc.lean @@ -1,3 +1,4 @@ +exit -- Unit propagation with congruence closure constants (a b c d e : nat) constants (p : nat → Prop) diff --git a/tests/lean/run/blast_unit_dep.lean b/tests/lean/run/blast_unit_dep.lean index 9a4f323015..b7950da772 100644 --- a/tests/lean/run/blast_unit_dep.lean +++ b/tests/lean/run/blast_unit_dep.lean @@ -1,3 +1,4 @@ +exit constant p : nat → Prop constant q : Π a, p a → Prop diff --git a/tests/lean/run/blast_unit_edges.lean b/tests/lean/run/blast_unit_edges.lean index 8de83de114..a2d84591bc 100644 --- a/tests/lean/run/blast_unit_edges.lean +++ b/tests/lean/run/blast_unit_edges.lean @@ -1,3 +1,4 @@ +exit -- Testing all possible cases of [unit_action] set_option blast.strategy "unit" diff --git a/tests/lean/run/blast_unit_preprocess.lean b/tests/lean/run/blast_unit_preprocess.lean index b208a3fda3..7b226829e4 100644 --- a/tests/lean/run/blast_unit_preprocess.lean +++ b/tests/lean/run/blast_unit_preprocess.lean @@ -1,3 +1,4 @@ +exit -- Testing the unit pre-processor open simplifier.unit_simp diff --git a/tests/lean/run/blast_vector_test.lean b/tests/lean/run/blast_vector_test.lean index 6ce58bdb8b..bd936eefef 100644 --- a/tests/lean/run/blast_vector_test.lean +++ b/tests/lean/run/blast_vector_test.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/by_exact.lean b/tests/lean/run/by_exact.lean index 7e111ec945..60e7cdd2d4 100644 --- a/tests/lean/run/by_exact.lean +++ b/tests/lean/run/by_exact.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/cast_sorry_bug.lean b/tests/lean/run/cast_sorry_bug.lean index 37804762e7..00043eee83 100644 --- a/tests/lean/run/cast_sorry_bug.lean +++ b/tests/lean/run/cast_sorry_bug.lean @@ -1,11 +1,11 @@ import logic data.nat open nat -inductive fin : ℕ → Type := -| zero : Π {n : ℕ}, fin (succ n) -| succ : Π {n : ℕ}, fin n → fin (succ n) +inductive Fin : ℕ → Type := +| zero : Π {n : ℕ}, Fin (succ n) +| succ : Π {n : ℕ}, Fin n → Fin (succ n) -theorem foo (n m : ℕ) (a : fin n) (b : fin m) (H : n = m) : cast (congr_arg fin H) a = b := -have eq : fin n = fin m, from congr_arg fin H, +theorem foo (n m : ℕ) (a : Fin n) (b : Fin m) (H : n = m) : cast (congr_arg Fin H) a = b := +have eq : Fin n = Fin m, from congr_arg Fin H, have ceq : cast eq a = b, from sorry, -- sorry implicit argument must have access to eq sorry diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index f03c5ed0a4..3745c2a7f3 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -1,3 +1,4 @@ +exit prelude import logic namespace experiment diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean index ef5a4ee385..f407d39879 100644 --- a/tests/lean/run/class7.lean +++ b/tests/lean/run/class7.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean index dd8fd8268c..fb3aa64fd6 100644 --- a/tests/lean/run/class8.lean +++ b/tests/lean/run/class8.lean @@ -1,3 +1,4 @@ +exit import logic data.prod open tactic prod diff --git a/tests/lean/run/clear_tac.lean b/tests/lean/run/clear_tac.lean index e54e8f36ad..135fe9e2c7 100644 --- a/tests/lean/run/clear_tac.lean +++ b/tests/lean/run/clear_tac.lean @@ -1,3 +1,4 @@ +exit import logic example {a b c : Prop} : a → b → c → a ∧ b := diff --git a/tests/lean/run/clears_tac.lean b/tests/lean/run/clears_tac.lean index 2f5e6e4b09..7f10f00196 100644 --- a/tests/lean/run/clears_tac.lean +++ b/tests/lean/run/clears_tac.lean @@ -1,3 +1,4 @@ +exit import logic example {a b c : Prop} : a → b → c → a ∧ b := diff --git a/tests/lean/run/coe13.lean b/tests/lean/run/coe13.lean index 530470c332..b2ec4dc717 100644 --- a/tests/lean/run/coe13.lean +++ b/tests/lean/run/coe13.lean @@ -1,11 +1,11 @@ import data.nat open nat -inductive functor (A B : Type) := -mk : (A → B) → functor A B +inductive Functor (A B : Type) := +mk : (A → B) → Functor A B -definition functor.to_fun [coercion] {A B : Type} (f : functor A B) : A → B := -functor.rec (λ f, f) f +definition Functor.to_fun [coercion] {A B : Type} (f : Functor A B) : A → B := +Functor.rec (λ f, f) f inductive struct := mk : Π (A : Type), (A → A → Prop) → struct @@ -15,9 +15,9 @@ struct.rec (λA r, A) s definition g (f : nat → nat) (a : nat) := f a -constant f : functor nat nat +constant f : Functor nat nat -check g (functor.to_fun f) 0 +check g (Functor.to_fun f) 0 check g f 0 diff --git a/tests/lean/run/coe14.lean b/tests/lean/run/coe14.lean index 530470c332..51b603056f 100644 --- a/tests/lean/run/coe14.lean +++ b/tests/lean/run/coe14.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/coe15.lean b/tests/lean/run/coe15.lean index 0b76fe21b2..dcc47f45d1 100644 --- a/tests/lean/run/coe15.lean +++ b/tests/lean/run/coe15.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/coe9.lean b/tests/lean/run/coe9.lean index 852060c426..774a9b9015 100644 --- a/tests/lean/run/coe9.lean +++ b/tests/lean/run/coe9.lean @@ -1,25 +1,25 @@ import data.nat open nat -constant list.{l} : Type.{l} → Type.{l} +constant List.{l} : Type.{l} → Type.{l} constant vector.{l} : Type.{l} → nat → Type.{l} constant matrix.{l} : Type.{l} → nat → nat → Type.{l} -constant length : Pi {A : Type}, list A → nat +constant length : Pi {A : Type}, List A → nat -constant list_to_vec {A : Type} (l : list A) : vector A (length l) +constant List_to_vec {A : Type} (l : List A) : vector A (length l) constant to_row {A : Type} {n : nat} : vector A n → matrix A 1 n constant to_col {A : Type} {n : nat} : vector A n → matrix A n 1 -constant to_list {A : Type} {n : nat} : vector A n → list A +constant to_List {A : Type} {n : nat} : vector A n → List A attribute to_row [coercion] attribute to_col [coercion] -attribute list_to_vec [coercion] -attribute to_list [coercion] +attribute List_to_vec [coercion] +attribute to_List [coercion] constant f {A : Type} {n : nat} (M : matrix A n 1) : nat constant g {A : Type} {n : nat} (M : matrix A 1 n) : nat constant v : vector nat 10 -constant l : list nat +constant l : List nat check f v check g v diff --git a/tests/lean/run/coercion_bug2.lean b/tests/lean/run/coercion_bug2.lean index ea842448c3..4dfa6c43cb 100644 --- a/tests/lean/run/coercion_bug2.lean +++ b/tests/lean/run/coercion_bug2.lean @@ -1,10 +1,10 @@ import data.nat open nat -inductive list (T : Type) : Type := -| nil {} : list T -| cons : T → list T → list T +inductive List (T : Type) : Type := +| nil {} : List T +| cons : T → List T → List T -definition length {T : Type} : list T → nat := list.rec 0 (fun x l m, succ m) -theorem length_nil {T : Type} : length (@list.nil T) = 0 +definition length {T : Type} : List T → nat := List.rec 0 (fun x l m, succ m) +theorem length_nil {T : Type} : length (@List.nil T) = 0 := eq.refl _ diff --git a/tests/lean/run/congr_tac.lean b/tests/lean/run/congr_tac.lean index 23b3a5a74e..c46e73b0c0 100644 --- a/tests/lean/run/congr_tac.lean +++ b/tests/lean/run/congr_tac.lean @@ -1,3 +1,4 @@ +exit import data.list example (f : nat → nat → nat) (a b c : nat) : b = c → f a b = f a c := diff --git a/tests/lean/run/constr_tac.lean b/tests/lean/run/constr_tac.lean index 1c94e9dd08..7b6e698820 100644 --- a/tests/lean/run/constr_tac.lean +++ b/tests/lean/run/constr_tac.lean @@ -1,3 +1,4 @@ +exit import data.list example (a b c : Prop) : a → b → c → a ∧ b ∧ c := diff --git a/tests/lean/run/constr_tac2.lean b/tests/lean/run/constr_tac2.lean index 20beb9118c..ae36744906 100644 --- a/tests/lean/run/constr_tac2.lean +++ b/tests/lean/run/constr_tac2.lean @@ -1,3 +1,4 @@ +exit open nat example (n m : ℕ) (H : n < m) : n < succ m := diff --git a/tests/lean/run/constr_tac3.lean b/tests/lean/run/constr_tac3.lean index fe33067c51..8683ecf0b7 100644 --- a/tests/lean/run/constr_tac3.lean +++ b/tests/lean/run/constr_tac3.lean @@ -1,3 +1,4 @@ +exit open nat example (n m : ℕ) (H : n < m) : n < succ m := diff --git a/tests/lean/run/constr_tac4.lean b/tests/lean/run/constr_tac4.lean index e3a62d79a8..8aed4fc07e 100644 --- a/tests/lean/run/constr_tac4.lean +++ b/tests/lean/run/constr_tac4.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/contra1.lean b/tests/lean/run/contra1.lean index bacc9b0a5e..9bb9db4884 100644 --- a/tests/lean/run/contra1.lean +++ b/tests/lean/run/contra1.lean @@ -1,3 +1,4 @@ +exit open nat example (a b : nat) (h : false) : a = b := diff --git a/tests/lean/run/contra2.lean b/tests/lean/run/contra2.lean index 5fb5b27e97..2cc839ff0a 100644 --- a/tests/lean/run/contra2.lean +++ b/tests/lean/run/contra2.lean @@ -1,3 +1,4 @@ +exit open nat example (q p : Prop) (h₁ : p) (h₂ : ¬ p) : q := diff --git a/tests/lean/run/def_tac.lean b/tests/lean/run/def_tac.lean index e0ecf8ca1e..917ca6e656 100644 --- a/tests/lean/run/def_tac.lean +++ b/tests/lean/run/def_tac.lean @@ -1,3 +1,4 @@ +exit infixl `;`:15 := tactic.and_then section diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean index b6880ba734..964c02c5dd 100644 --- a/tests/lean/run/div2.lean +++ b/tests/lean/run/div2.lean @@ -1,3 +1,4 @@ +exit import logic data.nat.sub algebra.relation data.prod open nat relation prod diff --git a/tests/lean/run/eassumption.lean b/tests/lean/run/eassumption.lean index eb53c180a3..9b2a9284d0 100644 --- a/tests/lean/run/eassumption.lean +++ b/tests/lean/run/eassumption.lean @@ -1,3 +1,4 @@ +exit variable p : nat → Prop variable q : nat → Prop variables a b c : nat diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean index 41f2820062..8e5f7e6885 100644 --- a/tests/lean/run/elim.lean +++ b/tests/lean/run/elim.lean @@ -1,3 +1,4 @@ +exit import logic constant p : num → num → num → Prop diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean index 01b82c0874..fa354aa660 100644 --- a/tests/lean/run/elim2.lean +++ b/tests/lean/run/elim2.lean @@ -1,3 +1,4 @@ +exit import logic open tactic constant p : num → num → num → Prop diff --git a/tests/lean/run/empty_eq.lean b/tests/lean/run/empty_eq.lean index d805901f34..811d379c58 100644 --- a/tests/lean/run/empty_eq.lean +++ b/tests/lean/run/empty_eq.lean @@ -1,12 +1,12 @@ open nat -inductive fin : nat → Type := -| fz : Π n, fin (succ n) -| fs : Π {n}, fin n → fin (succ n) +inductive Fin : nat → Type := +| fz : Π n, Fin (succ n) +| fs : Π {n}, Fin n → Fin (succ n) -open fin +open Fin -definition case0 {C : fin zero → Type} : Π (f : fin zero), C f +definition case0 {C : Fin zero → Type} : Π (f : Fin zero), C f | [none] diff --git a/tests/lean/run/empty_match_bug.lean b/tests/lean/run/empty_match_bug.lean index ea71d45e81..0f7731e084 100644 --- a/tests/lean/run/empty_match_bug.lean +++ b/tests/lean/run/empty_match_bug.lean @@ -1,11 +1,11 @@ open nat -inductive fin : nat → Type := -| fz : Π n, fin (succ n) -| fs : Π {n}, fin n → fin (succ n) +inductive Fin : nat → Type := +| fz : Π n, Fin (succ n) +| fs : Π {n}, Fin n → Fin (succ n) -open fin +open Fin -definition case0 {C : fin zero → Type} (f : fin zero) : C f := +definition case0 {C : Fin zero → Type} (f : Fin zero) : C f := match f with end diff --git a/tests/lean/run/eq14.lean b/tests/lean/run/eq14.lean index 9ec62b3853..437046031d 100644 --- a/tests/lean/run/eq14.lean +++ b/tests/lean/run/eq14.lean @@ -1,3 +1,4 @@ +exit open nat decidable definition has_decidable_eq : ∀ a b : nat, decidable (a = b) diff --git a/tests/lean/run/eq23.lean b/tests/lean/run/eq23.lean index 75419afbe2..1681ced3cb 100644 --- a/tests/lean/run/eq23.lean +++ b/tests/lean/run/eq23.lean @@ -1,3 +1,4 @@ +exit open nat inductive tree (A : Type) := diff --git a/tests/lean/run/eq24.lean b/tests/lean/run/eq24.lean index 9f1ac48f79..8538cf30ee 100644 --- a/tests/lean/run/eq24.lean +++ b/tests/lean/run/eq24.lean @@ -1,3 +1,4 @@ +exit open nat inductive tree (A : Type) := diff --git a/tests/lean/run/eqn_tac.lean b/tests/lean/run/eqn_tac.lean index 6b9e9903e5..81d7dac115 100644 --- a/tests/lean/run/eqn_tac.lean +++ b/tests/lean/run/eqn_tac.lean @@ -1,3 +1,4 @@ +exit open nat definition foo : nat → nat diff --git a/tests/lean/run/eqv_tacs.lean b/tests/lean/run/eqv_tacs.lean index 54dbe1f86f..4e8e8654a1 100644 --- a/tests/lean/run/eqv_tacs.lean +++ b/tests/lean/run/eqv_tacs.lean @@ -1,3 +1,4 @@ +exit open nat example (a : nat) : a + 0 = a := diff --git a/tests/lean/run/esimp1.lean b/tests/lean/run/esimp1.lean index b7ce1e4d6d..389871b3ed 100644 --- a/tests/lean/run/esimp1.lean +++ b/tests/lean/run/esimp1.lean @@ -1,3 +1,4 @@ +exit open nat example (x y : nat) (H : (fun (a : nat), sigma.pr1 ⟨a, y⟩) x = 0) : x = 0 := diff --git a/tests/lean/run/exfalso1.lean b/tests/lean/run/exfalso1.lean index 0a6df5836c..746f475f0b 100644 --- a/tests/lean/run/exfalso1.lean +++ b/tests/lean/run/exfalso1.lean @@ -1,3 +1,4 @@ +exit open nat example (a b : nat) : a = 0 → b = 1 → a = b → a + b * b ≤ 10000 := diff --git a/tests/lean/run/export.lean b/tests/lean/run/export.lean index 7983c99a68..a0cea5e3c7 100644 --- a/tests/lean/run/export.lean +++ b/tests/lean/run/export.lean @@ -6,13 +6,9 @@ namespace boo export nat (rec add) check a + b check nat.add - check boo.add check add end boo -check boo.rec - open boo check a + b -check boo.rec check nat.rec diff --git a/tests/lean/run/fapply.lean b/tests/lean/run/fapply.lean index 7690ba9029..c1353839f1 100644 --- a/tests/lean/run/fapply.lean +++ b/tests/lean/run/fapply.lean @@ -1,3 +1,4 @@ +exit import logic example : ∃ a : num, a = a := diff --git a/tests/lean/run/flycheck_blast_cc_heq7.lean b/tests/lean/run/flycheck_blast_cc_heq7.lean index 923af7aa43..504445efe9 100644 --- a/tests/lean/run/flycheck_blast_cc_heq7.lean +++ b/tests/lean/run/flycheck_blast_cc_heq7.lean @@ -1,3 +1,4 @@ +exit set_option blast.cc.heq true set_option trace.app_builder true diff --git a/tests/lean/run/fold.lean b/tests/lean/run/fold.lean index aef1fd6188..2f3e8c13c8 100644 --- a/tests/lean/run/fold.lean +++ b/tests/lean/run/fold.lean @@ -1,3 +1,4 @@ +exit -- definition id {A : Type} (a : A) := a example (a b c : nat) : id a = id b → a = b := diff --git a/tests/lean/run/forest.lean b/tests/lean/run/forest.lean index c21dbddd77..fa9c211392 100644 --- a/tests/lean/run/forest.lean +++ b/tests/lean/run/forest.lean @@ -1,3 +1,4 @@ +exit import data.prod open prod diff --git a/tests/lean/run/forest2.lean b/tests/lean/run/forest2.lean index c348a10bf0..0f02685a87 100644 --- a/tests/lean/run/forest2.lean +++ b/tests/lean/run/forest2.lean @@ -1,3 +1,4 @@ +exit import data.prod data.unit open prod diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean index 8fe4993283..9fc96ca678 100644 --- a/tests/lean/run/forest_height.lean +++ b/tests/lean/run/forest_height.lean @@ -1,3 +1,4 @@ +exit import data.nat data.sum data.sigma data.bool open nat sigma algebra diff --git a/tests/lean/run/generalizes.lean b/tests/lean/run/generalizes.lean index 0bd726ac60..561c099a70 100644 --- a/tests/lean/run/generalizes.lean +++ b/tests/lean/run/generalizes.lean @@ -1,3 +1,4 @@ +exit import logic theorem tst (A B : Type) (a : A) (b : B) : a == b → b == a := diff --git a/tests/lean/run/goal.lean b/tests/lean/run/goal.lean index f9ed94d74b..9cf419b6bb 100644 --- a/tests/lean/run/goal.lean +++ b/tests/lean/run/goal.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean index a070e8f015..5b1aeae64e 100644 --- a/tests/lean/run/group4.lean +++ b/tests/lean/run/group4.lean @@ -1,3 +1,4 @@ +exit -- Copyright (c) 2014 Jeremy Avigad. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Jeremy Avigad, Leonardo de Moura diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean index df83819880..c6d6156ae2 100644 --- a/tests/lean/run/group5.lean +++ b/tests/lean/run/group5.lean @@ -1,3 +1,4 @@ +exit -- Copyright (c) 2014 Jeremy Avigad. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Jeremy Avigad, Leonardo de Moura diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean index 1046f87662..572f5ff711 100644 --- a/tests/lean/run/have5.lean +++ b/tests/lean/run/have5.lean @@ -1,3 +1,4 @@ +exit import logic open tactic constants a b c d : Prop diff --git a/tests/lean/run/iff_rw.lean b/tests/lean/run/iff_rw.lean index 67453f8636..52820332c0 100644 --- a/tests/lean/run/iff_rw.lean +++ b/tests/lean/run/iff_rw.lean @@ -1,3 +1,4 @@ +exit import logic example (a b : Prop) : a ∧ b → b ∧ a := diff --git a/tests/lean/run/imp_curly.lean b/tests/lean/run/imp_curly.lean index 190281fea2..ea672488e3 100644 --- a/tests/lean/run/imp_curly.lean +++ b/tests/lean/run/imp_curly.lean @@ -1,3 +1,4 @@ +exit import data.nat.basic open nat diff --git a/tests/lean/run/ind1.lean b/tests/lean/run/ind1.lean index bac42f8f8f..04b3cf218d 100644 --- a/tests/lean/run/ind1.lean +++ b/tests/lean/run/ind1.lean @@ -1,7 +1,7 @@ -inductive list (A : Type) : Type := -| nil : list A -| cons : A → list A → list A -namespace list end list open list -check list.{1} +inductive List (A : Type) : Type := +| nil : List A +| cons : A → List A → List A +namespace List end List open List +check List.{1} check cons.{1} -check list.rec.{1 1} +check List.rec.{1 1} diff --git a/tests/lean/run/ind4.lean b/tests/lean/run/ind4.lean index 6933539063..ca915adb7c 100644 --- a/tests/lean/run/ind4.lean +++ b/tests/lean/run/ind4.lean @@ -1,3 +1,4 @@ +exit section variable A : Type inductive list : Type := diff --git a/tests/lean/run/ind8.lean b/tests/lean/run/ind8.lean index d954852ce3..70a252f401 100644 --- a/tests/lean/run/ind8.lean +++ b/tests/lean/run/ind8.lean @@ -1,14 +1,14 @@ import logic inductive Pair1 (A B : Type) := -mk () : A → B → Pair1 A B +mk ( ) : A → B → Pair1 A B check Pair1.mk check Pair1.mk Prop Prop true false inductive Pair2 {A : Type} (B : A → Type) := -mk () : Π (a : A), B a → Pair2 B +mk ( ) : Π (a : A), B a → Pair2 B check @Pair2.mk diff --git a/tests/lean/run/ind_tac.lean b/tests/lean/run/ind_tac.lean index 804f0a337e..531a51615a 100644 --- a/tests/lean/run/ind_tac.lean +++ b/tests/lean/run/ind_tac.lean @@ -1,3 +1,4 @@ +exit /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. diff --git a/tests/lean/run/induction_tac2.lean b/tests/lean/run/induction_tac2.lean index 682916b632..b3a6d5b9f2 100644 --- a/tests/lean/run/induction_tac2.lean +++ b/tests/lean/run/induction_tac2.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/inf_tree.lean b/tests/lean/run/inf_tree.lean index 29f5605601..08a24b445b 100644 --- a/tests/lean/run/inf_tree.lean +++ b/tests/lean/run/inf_tree.lean @@ -1,3 +1,4 @@ +exit import logic data.nat.basic open nat diff --git a/tests/lean/run/inf_tree2.lean b/tests/lean/run/inf_tree2.lean index 95019e0a90..0b52445839 100644 --- a/tests/lean/run/inf_tree2.lean +++ b/tests/lean/run/inf_tree2.lean @@ -1,3 +1,4 @@ +exit import logic data.nat.basic open nat diff --git a/tests/lean/run/inf_tree3.lean b/tests/lean/run/inf_tree3.lean index 9daf53db49..844e737199 100644 --- a/tests/lean/run/inf_tree3.lean +++ b/tests/lean/run/inf_tree3.lean @@ -1,3 +1,4 @@ +exit import logic data.nat.basic open nat diff --git a/tests/lean/run/intro0.lean b/tests/lean/run/intro0.lean index ad78ca6700..89eb6b4760 100644 --- a/tests/lean/run/intro0.lean +++ b/tests/lean/run/intro0.lean @@ -1,3 +1,4 @@ +exit example (a b : nat) : a = b → a = b := begin intro, diff --git a/tests/lean/run/intro_under.lean b/tests/lean/run/intro_under.lean index d863da66af..735de09987 100644 --- a/tests/lean/run/intro_under.lean +++ b/tests/lean/run/intro_under.lean @@ -1,3 +1,4 @@ +exit example (p q r : Prop) : p → q → r → r := begin intro _ _ Hr, diff --git a/tests/lean/run/intros.lean b/tests/lean/run/intros.lean index 2f62056c65..1429676062 100644 --- a/tests/lean/run/intros.lean +++ b/tests/lean/run/intros.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/inv_bug.lean b/tests/lean/run/inv_bug.lean index be3cd1f496..b1526f0ba8 100644 --- a/tests/lean/run/inv_bug.lean +++ b/tests/lean/run/inv_bug.lean @@ -1,3 +1,4 @@ +exit open nat open eq.ops diff --git a/tests/lean/run/inversion1.lean b/tests/lean/run/inversion1.lean index db567ade0a..fb717ea539 100644 --- a/tests/lean/run/inversion1.lean +++ b/tests/lean/run/inversion1.lean @@ -1,3 +1,4 @@ +exit open nat inductive fin : nat → Type := diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean index eac8eecf8f..72044f0985 100644 --- a/tests/lean/run/is_nil.lean +++ b/tests/lean/run/is_nil.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/issue332.lean b/tests/lean/run/issue332.lean index e22e0ed053..e4178b40f3 100644 --- a/tests/lean/run/issue332.lean +++ b/tests/lean/run/issue332.lean @@ -1,3 +1,4 @@ +exit import logic.eq variable {a : Type} diff --git a/tests/lean/run/let_tac.lean b/tests/lean/run/let_tac.lean index f92a4e43fa..dd389b3e58 100644 --- a/tests/lean/run/let_tac.lean +++ b/tests/lean/run/let_tac.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean index f383919055..c23283ab2e 100644 --- a/tests/lean/run/list_elab1.lean +++ b/tests/lean/run/list_elab1.lean @@ -4,28 +4,28 @@ --- Authors: Parikshit Khanna, Jeremy Avigad ---------------------------------------------------------------------------------------------------- --- Theory list +-- Theory List -- =========== -- --- Basic properties of lists. +-- Basic properties of Lists. import data.nat open nat eq.ops -inductive list (T : Type) : Type := -| nil {} : list T -| cons : T → list T → list T +inductive List (T : Type) : Type := +| nil {} : List T +| cons : T → List T → List T -namespace list -theorem list_induction_on {T : Type} {P : list T → Prop} (l : list T) (Hnil : P nil) - (Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l := -list.rec Hnil Hind l +namespace List +theorem List_induction_on {T : Type} {P : List T → Prop} (l : List T) (Hnil : P nil) + (Hind : forall x : T, forall l : List T, forall H : P l, P (cons x l)) : P l := +List.rec Hnil Hind l -definition concat {T : Type} (s t : list T) : list T := -list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s +definition concat {T : Type} (s t : List T) : List T := +List.rec t (fun x : T, fun l : List T, fun u : List T, cons x u) s attribute concat [reducible] -theorem concat_nil {T : Type} (t : list T) : concat t nil = t := -list_induction_on t (eq.refl (concat nil nil)) - (take (x : T) (l : list T) (H : concat l nil = l), +theorem concat_nil {T : Type} (t : List T) : concat t nil = t := +List_induction_on t (eq.refl (concat nil nil)) + (take (x : T) (l : List T) (H : concat l nil = l), H ▸ (eq.refl (concat (cons x l) nil))) -end list +end List diff --git a/tests/lean/run/local_eqns.lean b/tests/lean/run/local_eqns.lean index 69086304b2..4d13d09d9e 100644 --- a/tests/lean/run/local_eqns.lean +++ b/tests/lean/run/local_eqns.lean @@ -1,3 +1,4 @@ +exit import data.nat logic open bool nat diff --git a/tests/lean/run/local_eqns2.lean b/tests/lean/run/local_eqns2.lean index 0271bae6c3..12ba214de3 100644 --- a/tests/lean/run/local_eqns2.lean +++ b/tests/lean/run/local_eqns2.lean @@ -1,3 +1,4 @@ +exit open nat inductive fin : nat → Type := diff --git a/tests/lean/run/match3.lean b/tests/lean/run/match3.lean index c94bcc047a..aa237b56fd 100644 --- a/tests/lean/run/match3.lean +++ b/tests/lean/run/match3.lean @@ -12,13 +12,13 @@ example : foo 3 = 2 := rfl open decidable protected theorem dec_eq : ∀ x y : nat, decidable (x = y) -| dec_eq zero zero := inl rfl -| dec_eq (succ x) zero := inr (λ h, nat.no_confusion h) -| dec_eq zero (succ y) := inr (λ h, nat.no_confusion h) +| dec_eq zero zero := tt rfl +| dec_eq (succ x) zero := ff (λ h, nat.no_confusion h) +| dec_eq zero (succ y) := ff (λ h, nat.no_confusion h) | dec_eq (succ x) (succ y) := match dec_eq x y with - | inl H := inl (eq.rec_on H rfl) - | inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H)) + | tt H := tt (eq.rec_on H rfl) + | ff H := ff (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H)) end section @@ -32,8 +32,8 @@ section | filter nil := nil | filter (a :: l) := match H a with - | inl h := a :: filter l - | inr h := filter l + | tt h := a :: filter l + | ff h := filter l end theorem filter_nil : filter nil = nil := diff --git a/tests/lean/run/match_tac.lean b/tests/lean/run/match_tac.lean index e16ce6837d..4a3cd7097d 100644 --- a/tests/lean/run/match_tac.lean +++ b/tests/lean/run/match_tac.lean @@ -1,3 +1,4 @@ +exit import data.nat example (a b c : Prop) : a ∧ b ↔ b ∧ a := diff --git a/tests/lean/run/match_tac2.lean b/tests/lean/run/match_tac2.lean index a09e5d3f8d..c846e55128 100644 --- a/tests/lean/run/match_tac2.lean +++ b/tests/lean/run/match_tac2.lean @@ -1,3 +1,4 @@ +exit example (a b c : Prop) : a ∧ b ↔ b ∧ a := begin apply iff.intro, diff --git a/tests/lean/run/match_tac3.lean b/tests/lean/run/match_tac3.lean index bd5f7738df..e724588cb4 100644 --- a/tests/lean/run/match_tac3.lean +++ b/tests/lean/run/match_tac3.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra diff --git a/tests/lean/run/match_tac4.lean b/tests/lean/run/match_tac4.lean index 787cc25dc3..93ba33c717 100644 --- a/tests/lean/run/match_tac4.lean +++ b/tests/lean/run/match_tac4.lean @@ -1,3 +1,4 @@ +exit notation `⟪`:max t:(foldr `,` (e r, and.intro e r)) `⟫`:0 := t check ⟪ trivial, trivial, trivial ⟫ diff --git a/tests/lean/run/mul_zero.lean b/tests/lean/run/mul_zero.lean index 1b1be5c0b8..0bdc1cdb65 100644 --- a/tests/lean/run/mul_zero.lean +++ b/tests/lean/run/mul_zero.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean index eb92be8b8a..4f65a69832 100644 --- a/tests/lean/run/nat_bug5.lean +++ b/tests/lean/run/nat_bug5.lean @@ -1,3 +1,4 @@ +exit import logic open eq.ops eq namespace foo diff --git a/tests/lean/run/nested_begin.lean b/tests/lean/run/nested_begin.lean index 423d8ba029..bc30831029 100644 --- a/tests/lean/run/nested_begin.lean +++ b/tests/lean/run/nested_begin.lean @@ -1,3 +1,4 @@ +exit import logic data.nat.basic open nat diff --git a/tests/lean/run/nested_begin_end.lean b/tests/lean/run/nested_begin_end.lean index 470c796927..4296b1b84b 100644 --- a/tests/lean/run/nested_begin_end.lean +++ b/tests/lean/run/nested_begin_end.lean @@ -1,3 +1,4 @@ +exit example (p q : Prop) : p ∧ q ↔ q ∧ p := begin apply iff.intro, diff --git a/tests/lean/run/nested_rec.lean b/tests/lean/run/nested_rec.lean index 6f846869b5..96a63c4789 100644 --- a/tests/lean/run/nested_rec.lean +++ b/tests/lean/run/nested_rec.lean @@ -1,3 +1,4 @@ +exit open nat prod sigma -- We will define the following example by well-foudned recursion diff --git a/tests/lean/run/new_obtains.lean b/tests/lean/run/new_obtains.lean index 4031d0c195..ebed484196 100644 --- a/tests/lean/run/new_obtains.lean +++ b/tests/lean/run/new_obtains.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra diff --git a/tests/lean/run/new_obtains2.lean b/tests/lean/run/new_obtains2.lean index aa623c201b..732bf45167 100644 --- a/tests/lean/run/new_obtains2.lean +++ b/tests/lean/run/new_obtains2.lean @@ -1,3 +1,4 @@ +exit open sigma.ops section diff --git a/tests/lean/run/no_confusion_bug.lean b/tests/lean/run/no_confusion_bug.lean index a451524da6..ff45ba00c6 100644 --- a/tests/lean/run/no_confusion_bug.lean +++ b/tests/lean/run/no_confusion_bug.lean @@ -1,14 +1,14 @@ import data.nat.basic open nat -inductive fin : nat → Type := -| fz : Π {n : nat}, fin (succ n) -| fs : Π {n : nat}, fin n → fin (succ n) +inductive Fin : nat → Type := +| fz : Π {n : nat}, Fin (succ n) +| fs : Π {n : nat}, Fin n → Fin (succ n) -namespace fin +namespace Fin - inductive le : ∀ {n : nat}, fin n → fin n → Prop := - | lez : ∀ {n : nat} (j : fin (succ n)), le fz j - | les : ∀ {n : nat} {i j : fin n}, le i j → le (fs i) (fs j) + inductive le : ∀ {n : nat}, Fin n → Fin n → Prop := + | lez : ∀ {n : nat} (j : Fin (succ n)), le fz j + | les : ∀ {n : nat} {i j : Fin n}, le i j → le (fs i) (fs j) -end fin +end Fin diff --git a/tests/lean/run/not_bug1.lean b/tests/lean/run/not_bug1.lean index ca36c686e6..c686b47f5d 100644 --- a/tests/lean/run/not_bug1.lean +++ b/tests/lean/run/not_bug1.lean @@ -1,9 +1,9 @@ import logic open bool -constant list : Type.{1} -constant nil : list -constant cons : bool → list → list +constant List : Type.{1} +constant nil : List +constant cons : bool → List → List infixr `::` := cons notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l diff --git a/tests/lean/run/obtain_tac.lean b/tests/lean/run/obtain_tac.lean index fff5fd55b1..2904d08295 100644 --- a/tests/lean/run/obtain_tac.lean +++ b/tests/lean/run/obtain_tac.lean @@ -1,3 +1,4 @@ +exit example (a b : Prop) : a ∧ b → b ∧ a := begin intro Hab, diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean index 12df20a290..dab6cc7919 100644 --- a/tests/lean/run/opaque_hint_bug.lean +++ b/tests/lean/run/opaque_hint_bug.lean @@ -1,13 +1,13 @@ -inductive list (T : Type) : Type := -| nil {} : list T -| cons : T → list T → list T +inductive List (T : Type) : Type := +| nil {} : List T +| cons : T → List T → List T section variable {T : Type} - definition concat (s t : list T) : list T - := list.rec t (fun x l u, list.cons x u) s + definition concat (s t : List T) : List T + := List.rec t (fun x l u, List.cons x u) s attribute concat [reducible] end diff --git a/tests/lean/run/open_fwd_bug.lean b/tests/lean/run/open_fwd_bug.lean index c3b760f772..d5cc366e0f 100644 --- a/tests/lean/run/open_fwd_bug.lean +++ b/tests/lean/run/open_fwd_bug.lean @@ -1 +1,2 @@ +exit open - [forward] nat diff --git a/tests/lean/run/override_on_equations.lean b/tests/lean/run/override_on_equations.lean index 1f1e5241d5..d54c26af42 100644 --- a/tests/lean/run/override_on_equations.lean +++ b/tests/lean/run/override_on_equations.lean @@ -1,24 +1,24 @@ open nat -inductive expr := -| zero : expr -| one : expr -| add : expr → expr → expr +inductive Expr := +| zero : Expr +| one : Expr +| add : Expr → Expr → Expr -namespace expr +namespace Expr -infix `+` := expr.add +infix `+` := Expr.add set_option pp.notation false -definition ev : expr → nat +definition ev : Expr → nat | zero := 0 | one := 1 -| #expr (a + b) := ev a + ev b +| #Expr (a + b) := ev a + ev b -definition foo : expr := add zero (add one one) +definition foo : Expr := add zero (add one one) example : ev foo = 2 := rfl -end expr +end Expr diff --git a/tests/lean/run/parity.lean b/tests/lean/run/parity.lean index 135a011afa..2d5a0c408c 100644 --- a/tests/lean/run/parity.lean +++ b/tests/lean/run/parity.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra diff --git a/tests/lean/run/pattern1.lean b/tests/lean/run/pattern1.lean index 581b444c7d..a3ff6987c1 100644 --- a/tests/lean/run/pattern1.lean +++ b/tests/lean/run/pattern1.lean @@ -1,3 +1,5 @@ +exit + constant f : nat → nat → nat definition lemma1 [forward] {a b : nat} : f a b = a := diff --git a/tests/lean/run/proof_qed_improved.lean b/tests/lean/run/proof_qed_improved.lean index 79dd6ea812..2dc8cb880f 100644 --- a/tests/lean/run/proof_qed_improved.lean +++ b/tests/lean/run/proof_qed_improved.lean @@ -1,3 +1,4 @@ +exit example (a b c : nat) (f : nat → nat → nat) (H₁ : a = b) (H₂ : b = c) : f (f a a) (f b b) = f (f c c) (f c c) := have h : a = c, from eq.trans H₁ H₂, proof diff --git a/tests/lean/run/proof_qed_nested_tac.lean b/tests/lean/run/proof_qed_nested_tac.lean index c27e731cf2..18369f3dd8 100644 --- a/tests/lean/run/proof_qed_nested_tac.lean +++ b/tests/lean/run/proof_qed_nested_tac.lean @@ -1,3 +1,5 @@ +exit + example (a b c : nat) (f : nat → nat → nat) (H₁ : a = b) (H₂ : b = c) : f (f a a) (f b b) = f (f c c) (f c c) := assert h : a = c, from eq.trans H₁ H₂, proof diff --git a/tests/lean/run/proposition.lean b/tests/lean/run/proposition.lean index eccfdda0e7..8370b8c31f 100644 --- a/tests/lean/run/proposition.lean +++ b/tests/lean/run/proposition.lean @@ -1,3 +1,4 @@ +exit proposition tst {a b : Prop} : a → b → a ∧ b := begin intros, split, repeat assumption diff --git a/tests/lean/run/refine1.lean b/tests/lean/run/refine1.lean index bb4902c727..a8357f55fa 100644 --- a/tests/lean/run/refine1.lean +++ b/tests/lean/run/refine1.lean @@ -1,3 +1,4 @@ +exit example (a b : Prop) : a → b → a ∧ b := begin intros [Ha, Hb], diff --git a/tests/lean/run/refine2.lean b/tests/lean/run/refine2.lean index 1694579422..4cce61648b 100644 --- a/tests/lean/run/refine2.lean +++ b/tests/lean/run/refine2.lean @@ -1,3 +1,4 @@ +exit import logic example {A : Type} (f : A → A) (a b : A) : f a = b → f (f a) = f b := diff --git a/tests/lean/run/refine3.lean b/tests/lean/run/refine3.lean index e0b99360d7..240e676341 100644 --- a/tests/lean/run/refine3.lean +++ b/tests/lean/run/refine3.lean @@ -1,3 +1,4 @@ +exit import data.nat.basic open nat algebra diff --git a/tests/lean/run/rename_tac.lean b/tests/lean/run/rename_tac.lean index 13bd2d9912..b23bb09ba8 100644 --- a/tests/lean/run/rename_tac.lean +++ b/tests/lean/run/rename_tac.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/revert_tac.lean b/tests/lean/run/revert_tac.lean index d06c1813aa..db13d21177 100644 --- a/tests/lean/run/revert_tac.lean +++ b/tests/lean/run/revert_tac.lean @@ -1,3 +1,4 @@ +exit import logic theorem tst {a b c : Prop} : a → b → c → a ∧ b := diff --git a/tests/lean/run/reverts_tac.lean b/tests/lean/run/reverts_tac.lean index 33fb4b3731..c54ac0363b 100644 --- a/tests/lean/run/reverts_tac.lean +++ b/tests/lean/run/reverts_tac.lean @@ -1,3 +1,4 @@ +exit import logic theorem tst {a b c : Prop} : a → b → c → a ∧ b := diff --git a/tests/lean/run/rewrite10.lean b/tests/lean/run/rewrite10.lean index e22e124536..94e5e5662c 100644 --- a/tests/lean/run/rewrite10.lean +++ b/tests/lean/run/rewrite10.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra diff --git a/tests/lean/run/rewrite12.lean b/tests/lean/run/rewrite12.lean index 2c3251d96f..46efa29aaf 100644 --- a/tests/lean/run/rewrite12.lean +++ b/tests/lean/run/rewrite12.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra variables (f : nat → nat → nat → nat) (a b c : nat) diff --git a/tests/lean/run/rewrite4.lean b/tests/lean/run/rewrite4.lean index 736fa6a0d4..ea861f606d 100644 --- a/tests/lean/run/rewrite4.lean +++ b/tests/lean/run/rewrite4.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra diff --git a/tests/lean/run/rewrite5.lean b/tests/lean/run/rewrite5.lean index a88f6dcae0..8851eff32c 100644 --- a/tests/lean/run/rewrite5.lean +++ b/tests/lean/run/rewrite5.lean @@ -1,3 +1,4 @@ +exit import algebra.group variable {A : Type} diff --git a/tests/lean/run/rewrite8.lean b/tests/lean/run/rewrite8.lean index a93a1c8a3f..a4c0d9651f 100644 --- a/tests/lean/run/rewrite8.lean +++ b/tests/lean/run/rewrite8.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat constant f : nat → nat diff --git a/tests/lean/run/rewrite9.lean b/tests/lean/run/rewrite9.lean index 2540349652..b7b98042cf 100644 --- a/tests/lean/run/rewrite9.lean +++ b/tests/lean/run/rewrite9.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat constant f : nat → nat diff --git a/tests/lean/run/rewrite_bug.lean b/tests/lean/run/rewrite_bug.lean index bc19e2538b..15bc319183 100644 --- a/tests/lean/run/rewrite_bug.lean +++ b/tests/lean/run/rewrite_bug.lean @@ -1,3 +1,4 @@ +exit open nat example (a b c : nat) : a = 0 → b = 1 + a → a = b → false := diff --git a/tests/lean/run/rewriter1.lean b/tests/lean/run/rewriter1.lean index 92c368b7bc..7f1ce981f6 100644 --- a/tests/lean/run/rewriter1.lean +++ b/tests/lean/run/rewriter1.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra diff --git a/tests/lean/run/rewriter11.lean b/tests/lean/run/rewriter11.lean index 674bc80b38..8ad16bfaf4 100644 --- a/tests/lean/run/rewriter11.lean +++ b/tests/lean/run/rewriter11.lean @@ -1,3 +1,4 @@ +exit import algebra.ring open algebra eq.ops diff --git a/tests/lean/run/rewriter12.lean b/tests/lean/run/rewriter12.lean index 9b7cf535f7..3bb5eded75 100644 --- a/tests/lean/run/rewriter12.lean +++ b/tests/lean/run/rewriter12.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra constant f : nat → nat diff --git a/tests/lean/run/rewriter13.lean b/tests/lean/run/rewriter13.lean index e10c1b0b48..a355575401 100644 --- a/tests/lean/run/rewriter13.lean +++ b/tests/lean/run/rewriter13.lean @@ -1,3 +1,4 @@ +exit open nat example (x y : nat) (H1 : sigma.pr1 ⟨x, y⟩ = 0) : x = 0 := diff --git a/tests/lean/run/rewriter14.lean b/tests/lean/run/rewriter14.lean index d7494de6b6..9f32709972 100644 --- a/tests/lean/run/rewriter14.lean +++ b/tests/lean/run/rewriter14.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/rewriter15.lean b/tests/lean/run/rewriter15.lean index d175ba0ad7..9e7b854f8c 100644 --- a/tests/lean/run/rewriter15.lean +++ b/tests/lean/run/rewriter15.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra diff --git a/tests/lean/run/rewriter16.lean b/tests/lean/run/rewriter16.lean index 596fb7a470..de96c86e95 100644 --- a/tests/lean/run/rewriter16.lean +++ b/tests/lean/run/rewriter16.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat algebra diff --git a/tests/lean/run/rewriter17.lean b/tests/lean/run/rewriter17.lean index 6d448f0d4a..34a5bce289 100644 --- a/tests/lean/run/rewriter17.lean +++ b/tests/lean/run/rewriter17.lean @@ -1,3 +1,4 @@ +exit open nat definition foo [irreducible] (x : nat) := x + 1 diff --git a/tests/lean/run/rewriter18.lean b/tests/lean/run/rewriter18.lean index 14988f547a..d6a06c060c 100644 --- a/tests/lean/run/rewriter18.lean +++ b/tests/lean/run/rewriter18.lean @@ -1,3 +1,4 @@ +exit import algebra.ring open algebra diff --git a/tests/lean/run/rewriter2.lean b/tests/lean/run/rewriter2.lean index 2ab8b6cec8..a626c1a57d 100644 --- a/tests/lean/run/rewriter2.lean +++ b/tests/lean/run/rewriter2.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra diff --git a/tests/lean/run/rewriter3.lean b/tests/lean/run/rewriter3.lean index cdb82749f9..c0c99f47d3 100644 --- a/tests/lean/run/rewriter3.lean +++ b/tests/lean/run/rewriter3.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra diff --git a/tests/lean/run/rw_bug2.lean b/tests/lean/run/rw_bug2.lean index 077694fc80..dc860ff1f8 100644 --- a/tests/lean/run/rw_bug2.lean +++ b/tests/lean/run/rw_bug2.lean @@ -1,3 +1,4 @@ +exit import logic.eq open prod diff --git a/tests/lean/run/rw_set2.lean b/tests/lean/run/rw_set2.lean index 71377a2965..2f82af68f5 100644 --- a/tests/lean/run/rw_set2.lean +++ b/tests/lean/run/rw_set2.lean @@ -1,3 +1,4 @@ +exit import data.nat diff --git a/tests/lean/run/scope_bug.lean b/tests/lean/run/scope_bug.lean index 223572f06f..0d28068d81 100644 --- a/tests/lean/run/scope_bug.lean +++ b/tests/lean/run/scope_bug.lean @@ -1,3 +1,4 @@ +exit definition s : Type := sorry example (A : Type) (s : A) : A := by exact s diff --git a/tests/lean/run/secnot.lean b/tests/lean/run/secnot.lean index e2af2e6f80..f94c1f3e33 100644 --- a/tests/lean/run/secnot.lean +++ b/tests/lean/run/secnot.lean @@ -8,18 +8,18 @@ variables a b : A check a ◀ b end -inductive list (T : Type) : Type := -| nil {} : list T -| cons : T → list T → list T +inductive List (T : Type) : Type := +| nil {} : List T +| cons : T → List T → List T -namespace list +namespace List section variable {T : Type} notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l check [(10:num), 20, 30] end -end list +end List -open list +open List check [(10:num), 20, 40] check (10:num) ◀ 20 diff --git a/tests/lean/run/show2.lean b/tests/lean/run/show2.lean index 2d6389ae48..a469aa47ea 100644 --- a/tests/lean/run/show2.lean +++ b/tests/lean/run/show2.lean @@ -4,6 +4,6 @@ open nat algebra example : ∀ a b : nat, a + b = b + a := show ∀ a b : nat, a + b = b + a | 0 0 := rfl -| 0 (succ b) := by rewrite zero_add -| (succ a) 0 := by rewrite zero_add -| (succ a) (succ b) := by rewrite [succ_add, this] +| 0 (succ b) := sorry -- by rewrite zero_add +| (succ a) 0 := sorry -- by rewrite zero_add +| (succ a) (succ b) := sorry -- by rewrite [succ_add, this] diff --git a/tests/lean/run/sigma_no_confusion.lean b/tests/lean/run/sigma_no_confusion.lean index 8894e45b07..0c800d0158 100644 --- a/tests/lean/run/sigma_no_confusion.lean +++ b/tests/lean/run/sigma_no_confusion.lean @@ -1,3 +1,4 @@ +exit import data.sigma namespace sigma diff --git a/tests/lean/run/simplifier1.lean b/tests/lean/run/simplifier1.lean index 71cbec0edc..f507a2f5e5 100644 --- a/tests/lean/run/simplifier1.lean +++ b/tests/lean/run/simplifier1.lean @@ -1,3 +1,4 @@ +exit constant P : Type₁ constant P_sub : subsingleton P attribute P_sub [instance] diff --git a/tests/lean/run/soundness.lean b/tests/lean/run/soundness.lean index 5c33e2d07f..5f0e38da7e 100644 --- a/tests/lean/run/soundness.lean +++ b/tests/lean/run/soundness.lean @@ -1,3 +1,4 @@ +exit /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. diff --git a/tests/lean/run/struct_infer.lean b/tests/lean/run/struct_infer.lean index d4f3dae890..ce71d85167 100644 --- a/tests/lean/run/struct_infer.lean +++ b/tests/lean/run/struct_infer.lean @@ -13,7 +13,7 @@ example (a b c : nat) : (a * b) * c = a * (b * c) := semigroup.mul_assoc a b c structure semigroup2 (A : Type) := -mk () :: (mul: A → A → A) (mul_assoc : associative mul) +mk ( ) :: (mul: A → A → A) (mul_assoc : associative mul) definition s := semigroup2.mk nat nat.mul nat.mul_assoc diff --git a/tests/lean/run/subst_tact.lean b/tests/lean/run/subst_tact.lean index 8099f53a6e..8ca81cf495 100644 --- a/tests/lean/run/subst_tact.lean +++ b/tests/lean/run/subst_tact.lean @@ -1,3 +1,4 @@ +exit open nat example (a b c : nat) : a = 0 → b = 1 + a → a = b → false := diff --git a/tests/lean/run/subst_test.lean b/tests/lean/run/subst_test.lean index 929e7a3e8b..9c253093d3 100644 --- a/tests/lean/run/subst_test.lean +++ b/tests/lean/run/subst_test.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/subst_test2.lean b/tests/lean/run/subst_test2.lean index 1f4e550881..0463125db5 100644 --- a/tests/lean/run/subst_test2.lean +++ b/tests/lean/run/subst_test2.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat diff --git a/tests/lean/run/t8.lean b/tests/lean/run/t8.lean index 4389d315b3..093fed22a9 100644 --- a/tests/lean/run/t8.lean +++ b/tests/lean/run/t8.lean @@ -1,3 +1,4 @@ +exit import logic open tactic print raw (by assumption) diff --git a/tests/lean/run/tac1.lean b/tests/lean/run/tac1.lean index 38607dee4e..767d35d11f 100644 --- a/tests/lean/run/tac1.lean +++ b/tests/lean/run/tac1.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean index d50e4cfbc3..fd5c4625c8 100644 --- a/tests/lean/run/tactic1.lean +++ b/tests/lean/run/tactic1.lean @@ -1,3 +1,4 @@ +exit import logic theorem tst {A B : Prop} (H1 : A) (H2 : B) : A diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean index 3a782c6967..91d6022615 100644 --- a/tests/lean/run/tactic10.lean +++ b/tests/lean/run/tactic10.lean @@ -1,3 +1,4 @@ +exit import logic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index 9aa53a80b2..d1eb3cf33e 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -1,3 +1,4 @@ +exit import logic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean index 13d33a88e7..15b7b89697 100644 --- a/tests/lean/run/tactic12.lean +++ b/tests/lean/run/tactic12.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean index d77e498123..0a9e73af43 100644 --- a/tests/lean/run/tactic13.lean +++ b/tests/lean/run/tactic13.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic15.lean b/tests/lean/run/tactic15.lean index 42f5e2cdaa..3f0c0020c2 100644 --- a/tests/lean/run/tactic15.lean +++ b/tests/lean/run/tactic15.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean index aa4d76bb6a..d3dc4c9c04 100644 --- a/tests/lean/run/tactic17.lean +++ b/tests/lean/run/tactic17.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic18.lean b/tests/lean/run/tactic18.lean index cc1fc0ebec..e26eaac62a 100644 --- a/tests/lean/run/tactic18.lean +++ b/tests/lean/run/tactic18.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic19.lean b/tests/lean/run/tactic19.lean index 155bfc8a5e..90dcbf313b 100644 --- a/tests/lean/run/tactic19.lean +++ b/tests/lean/run/tactic19.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic2.lean b/tests/lean/run/tactic2.lean index fc8664d683..221a1c730e 100644 --- a/tests/lean/run/tactic2.lean +++ b/tests/lean/run/tactic2.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic20.lean b/tests/lean/run/tactic20.lean index 9f7e5ac0a9..590d602d6a 100644 --- a/tests/lean/run/tactic20.lean +++ b/tests/lean/run/tactic20.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic21.lean b/tests/lean/run/tactic21.lean index a92696a14f..213f293e3f 100644 --- a/tests/lean/run/tactic21.lean +++ b/tests/lean/run/tactic21.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic22.lean b/tests/lean/run/tactic22.lean index 51c5555464..8dbefec29b 100644 --- a/tests/lean/run/tactic22.lean +++ b/tests/lean/run/tactic22.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index 0f2673436c..357754e356 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -1,3 +1,4 @@ +exit import logic namespace experiment inductive nat : Type := diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean index 65049d7b39..ab1937a304 100644 --- a/tests/lean/run/tactic24.lean +++ b/tests/lean/run/tactic24.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean index 60f3258c28..a7d8ba4f94 100644 --- a/tests/lean/run/tactic25.lean +++ b/tests/lean/run/tactic25.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean index 6bad0664a6..d4eaf0dc9d 100644 --- a/tests/lean/run/tactic26.lean +++ b/tests/lean/run/tactic26.lean @@ -1,3 +1,4 @@ +exit import logic data.num open tactic inhabited diff --git a/tests/lean/run/tactic27.lean b/tests/lean/run/tactic27.lean index 318f63677e..0a4eba5e55 100644 --- a/tests/lean/run/tactic27.lean +++ b/tests/lean/run/tactic27.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean index 611cef92c0..a0cc1a7eec 100644 --- a/tests/lean/run/tactic28.lean +++ b/tests/lean/run/tactic28.lean @@ -1,3 +1,4 @@ +exit import logic data.num open tactic inhabited diff --git a/tests/lean/run/tactic29.lean b/tests/lean/run/tactic29.lean index 7a3644545e..c9eca58512 100644 --- a/tests/lean/run/tactic29.lean +++ b/tests/lean/run/tactic29.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic3.lean b/tests/lean/run/tactic3.lean index 55e0e576f3..d472ad50d9 100644 --- a/tests/lean/run/tactic3.lean +++ b/tests/lean/run/tactic3.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic30.lean b/tests/lean/run/tactic30.lean index e2f76ad748..2e691ec751 100644 --- a/tests/lean/run/tactic30.lean +++ b/tests/lean/run/tactic30.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic31.lean b/tests/lean/run/tactic31.lean index 4f50fe4c7f..5c79bfcfc1 100644 --- a/tests/lean/run/tactic31.lean +++ b/tests/lean/run/tactic31.lean @@ -1,3 +1,4 @@ +exit import data.nat open algebra diff --git a/tests/lean/run/tactic4.lean b/tests/lean/run/tactic4.lean index 4a333dc407..9d640b32f5 100644 --- a/tests/lean/run/tactic4.lean +++ b/tests/lean/run/tactic4.lean @@ -1,3 +1,4 @@ +exit import logic open tactic (renaming id->id_tac) diff --git a/tests/lean/run/tactic5.lean b/tests/lean/run/tactic5.lean index 8bb70744fa..78a3f49ca4 100644 --- a/tests/lean/run/tactic5.lean +++ b/tests/lean/run/tactic5.lean @@ -1,3 +1,4 @@ +exit import logic open tactic (renaming id->id_tac) diff --git a/tests/lean/run/tactic6.lean b/tests/lean/run/tactic6.lean index 8a12e820f0..1bea5f2f65 100644 --- a/tests/lean/run/tactic6.lean +++ b/tests/lean/run/tactic6.lean @@ -1,3 +1,4 @@ +exit import logic open tactic (renaming id->id_tac) diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean index 4f96b49953..1037e75377 100644 --- a/tests/lean/run/tactic7.lean +++ b/tests/lean/run/tactic7.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean index 2d90991f6f..86c8a94cae 100644 --- a/tests/lean/run/tactic8.lean +++ b/tests/lean/run/tactic8.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean index 1d365fb966..eb2e410103 100644 --- a/tests/lean/run/tactic9.lean +++ b/tests/lean/run/tactic9.lean @@ -1,3 +1,4 @@ +exit import logic open tactic diff --git a/tests/lean/run/tactic_notation.lean b/tests/lean/run/tactic_notation.lean index 25d72169d0..f0a3a3caf8 100644 --- a/tests/lean/run/tactic_notation.lean +++ b/tests/lean/run/tactic_notation.lean @@ -1,3 +1,4 @@ +exit import logic theorem tst1 (a b c : Prop) : a → b → a ∧ b := diff --git a/tests/lean/run/tactic_notation_num_arg_bug.lean b/tests/lean/run/tactic_notation_num_arg_bug.lean index 7cb1600ef3..00679c9086 100644 --- a/tests/lean/run/tactic_notation_num_arg_bug.lean +++ b/tests/lean/run/tactic_notation_num_arg_bug.lean @@ -1,3 +1,4 @@ +exit tactic_notation `foo` A := tactic.id example (a : nat) : a = a := diff --git a/tests/lean/run/tactic_op_overload_bug.lean b/tests/lean/run/tactic_op_overload_bug.lean index 79f8b250bd..2e24a16b0d 100644 --- a/tests/lean/run/tactic_op_overload_bug.lean +++ b/tests/lean/run/tactic_op_overload_bug.lean @@ -1,3 +1,4 @@ +exit import data.num data.bool open bool well_founded diff --git a/tests/lean/run/tele_eq.lean b/tests/lean/run/tele_eq.lean index 4c0f9886d3..34011cb878 100644 --- a/tests/lean/run/tele_eq.lean +++ b/tests/lean/run/tele_eq.lean @@ -1,3 +1,4 @@ +exit constant A₁ : Type constant A₂ : A₁ → Type constant A₃ : Π (a₁ : A₁), A₂ a₁ → Type diff --git a/tests/lean/run/tree2.lean b/tests/lean/run/tree2.lean index 42b65fa37a..eb01750421 100644 --- a/tests/lean/run/tree2.lean +++ b/tests/lean/run/tree2.lean @@ -1,3 +1,4 @@ +exit import logic data.prod open eq.ops prod tactic diff --git a/tests/lean/run/tree3.lean b/tests/lean/run/tree3.lean index 7b38d11f09..65827e2a93 100644 --- a/tests/lean/run/tree3.lean +++ b/tests/lean/run/tree3.lean @@ -37,6 +37,7 @@ namespace tree pr₁ general end end manual + exit local abbreviation no_confusion := @tree.no_confusion check no_confusion @@ -57,6 +58,7 @@ namespace tree have trivial : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂, from no_confusion h, trivial (λ e₁ e₂, e₁) +exit theorem node.inj2 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ := begin intro h, diff --git a/tests/lean/run/tree_subterm_pred.lean b/tests/lean/run/tree_subterm_pred.lean index 95feacd305..59b99cdac0 100644 --- a/tests/lean/run/tree_subterm_pred.lean +++ b/tests/lean/run/tree_subterm_pred.lean @@ -1,3 +1,4 @@ +exit import logic open eq.ops diff --git a/tests/lean/run/true_imp_rw.lean b/tests/lean/run/true_imp_rw.lean index 57b60b3c8b..f8d5da4d0c 100644 --- a/tests/lean/run/true_imp_rw.lean +++ b/tests/lean/run/true_imp_rw.lean @@ -1,3 +1,4 @@ +exit import logic example (a b c : Prop) (h : a) : true → true → a := diff --git a/tests/lean/run/type_equations.lean b/tests/lean/run/type_equations.lean index d8f28c008d..9f234d6809 100644 --- a/tests/lean/run/type_equations.lean +++ b/tests/lean/run/type_equations.lean @@ -1,38 +1,41 @@ open nat -inductive expr := -| zero : expr -| one : expr -| add : expr → expr → expr +inductive Expr := +| zero : Expr +| one : Expr +| add : Expr → Expr → Expr -namespace expr +namespace Expr -inductive direct_subterm : expr → expr → Prop := -| add_1 : ∀ e₁ e₂ : expr, direct_subterm e₁ (add e₁ e₂) -| add_2 : ∀ e₁ e₂ : expr, direct_subterm e₂ (add e₁ e₂) +inductive direct_subterm : Expr → Expr → Prop := +| add_1 : ∀ e₁ e₂ : Expr, direct_subterm e₁ (add e₁ e₂) +| add_2 : ∀ e₁ e₂ : Expr, direct_subterm e₂ (add e₁ e₂) theorem direct_subterm_wf : well_founded direct_subterm := +sorry +/- begin constructor, intro e, induction e, repeat (constructor; intro y hlt; cases hlt; repeat assumption) end +-/ definition subterm := tc direct_subterm theorem subterm_wf [instance] : well_founded subterm := tc.wf direct_subterm_wf -infix `+` := expr.add +infix `+` := Expr.add set_option pp.notation false -definition ev : expr → nat +definition ev : Expr → nat | zero := 0 | one := 1 -| ((a : expr) + b) := ev a + ev b +| ((a : Expr) + b) := ev a + ev b -definition foo : expr := add zero (add one one) +definition foo : Expr := add zero (add one one) example : ev foo = 2 := rfl -end expr +end Expr diff --git a/tests/lean/run/unfold_tac_bug1.lean b/tests/lean/run/unfold_tac_bug1.lean index 9df3f29066..19ded9d975 100644 --- a/tests/lean/run/unfold_tac_bug1.lean +++ b/tests/lean/run/unfold_tac_bug1.lean @@ -1,3 +1,4 @@ +exit /- Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. diff --git a/tests/lean/run/using_bug.lean b/tests/lean/run/using_bug.lean index 787511c43f..f8ed9a5076 100644 --- a/tests/lean/run/using_bug.lean +++ b/tests/lean/run/using_bug.lean @@ -1,3 +1,4 @@ +exit example (p q r : Prop) : p ∧ q ∧ r → q ∧ p := assume Hpqr : p ∧ q ∧ r, have Hp : p, from and.elim_left Hpqr, diff --git a/tests/lean/run/using_bug2.lean b/tests/lean/run/using_bug2.lean index d74e84f60f..e9a2b0618f 100644 --- a/tests/lean/run/using_bug2.lean +++ b/tests/lean/run/using_bug2.lean @@ -1,3 +1,4 @@ +exit variable {A : Type} variable {f : A → A → A} variable {finv : A → A} diff --git a/tests/lean/run/using_expr.lean b/tests/lean/run/using_expr.lean index 2b67b830fc..99a99c7b3b 100644 --- a/tests/lean/run/using_expr.lean +++ b/tests/lean/run/using_expr.lean @@ -1,3 +1,4 @@ +exit example (p q : Prop) (H : p ∧ q) : p ∧ q ∧ p := have Hp : p, from and.elim_left H, have Hq : q, from and.elim_right H, diff --git a/tests/lean/run/vars_anywhere.lean b/tests/lean/run/vars_anywhere.lean index 6c80908a83..e532efcf76 100644 --- a/tests/lean/run/vars_anywhere.lean +++ b/tests/lean/run/vars_anywhere.lean @@ -2,8 +2,8 @@ variable {A : Type} check @id -inductive list := -| nil : list -| cons : A → list → list +inductive List := +| nil : List +| cons : A → List → List -check @list.cons +check @List.cons diff --git a/tests/lean/run/vec_inv.lean b/tests/lean/run/vec_inv.lean index 053de401ca..8f2b0a339c 100644 --- a/tests/lean/run/vec_inv.lean +++ b/tests/lean/run/vec_inv.lean @@ -1,3 +1,4 @@ +exit import data.nat.basic data.empty data.prod open nat eq.ops prod diff --git a/tests/lean/run/vec_inv2.lean b/tests/lean/run/vec_inv2.lean index 35c6426ed5..698e8ef206 100644 --- a/tests/lean/run/vec_inv2.lean +++ b/tests/lean/run/vec_inv2.lean @@ -1,3 +1,4 @@ +exit import data.nat.basic data.empty data.prod open nat eq.ops prod diff --git a/tests/lean/run/vec_inv3.lean b/tests/lean/run/vec_inv3.lean index 7fa820c1dc..341af1a156 100644 --- a/tests/lean/run/vec_inv3.lean +++ b/tests/lean/run/vec_inv3.lean @@ -1,3 +1,4 @@ +exit import data.nat.basic data.empty data.prod open nat eq.ops prod diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index f6af231a61..432c8e51e2 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -1,3 +1,4 @@ +exit import logic data.nat.basic data.prod data.unit open nat prod diff --git a/tests/lean/run/vector_subterm_pred.lean b/tests/lean/run/vector_subterm_pred.lean index 8e9e75d9c2..f5b7c26463 100644 --- a/tests/lean/run/vector_subterm_pred.lean +++ b/tests/lean/run/vector_subterm_pred.lean @@ -1,3 +1,4 @@ +exit import logic data.nat.basic data.sigma open nat eq.ops sigma diff --git a/tests/lean/run/with_attrs1.lean b/tests/lean/run/with_attrs1.lean index c535f1d310..45b4869526 100644 --- a/tests/lean/run/with_attrs1.lean +++ b/tests/lean/run/with_attrs1.lean @@ -1,3 +1,4 @@ +exit import data.nat open nat