From be5d034b6efa4c52690fa885e730eaef0e41ebd3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Aug 2014 16:04:23 -0700 Subject: [PATCH] chore(library/standard): remove workarounds Signed-off-by: Leonardo de Moura --- library/standard/data/list/basic.lean | 4 ---- library/standard/logic/axioms/examples/diaconescu.lean | 1 - 2 files changed, 5 deletions(-) diff --git a/library/standard/data/list/basic.lean b/library/standard/data/list/basic.lean index f4b93ebf4..f4e2c806a 100644 --- a/library/standard/data/list/basic.lean +++ b/library/standard/data/list/basic.lean @@ -221,9 +221,6 @@ list_induction_on s theorem mem_concat (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t := iff_intro (mem_concat_imp_or _ _ _) (mem_or_imp_concat _ _ _) -section -set_option unifier.expensive true -- TODO(Leo): remove after we add delta-split step -#erase_cache mem_split theorem mem_split (x : T) (l : list T) : x ∈ l → ∃s t : list T, l = s ++ (x :: t) := list_induction_on l (take H : x ∈ nil, false_elim _ (iff_elim_left (mem_nil x) H)) @@ -240,7 +237,6 @@ list_induction_on l have H4 : y :: l = (y :: s) ++ (x :: t), from subst H3 (refl (y :: l)), exists_intro _ (exists_intro _ H4))) -end -- Find -- ---- diff --git a/library/standard/logic/axioms/examples/diaconescu.lean b/library/standard/logic/axioms/examples/diaconescu.lean index 223d3014c..c0081207c 100644 --- a/library/standard/logic/axioms/examples/diaconescu.lean +++ b/library/standard/logic/axioms/examples/diaconescu.lean @@ -32,7 +32,6 @@ or_elim u_def (assume Hp : p, or_inr Hp)) (assume Hp : p, or_inr Hp) -set_option unifier.expensive true lemma p_implies_uv [private] : p → u = v := assume Hp : p, have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from