From 59b11c815cfa5244b901b87136a64a8a7cd411aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Apr 2015 14:02:19 -0700 Subject: [PATCH] refactor(library/data/list/perm): remove unnessary lambda abstractions The contradiction tactic takes care of it. --- library/data/list/perm.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 6125ea73d2..f6f1506c70 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -24,17 +24,17 @@ theorem eq_nil_of_perm_nil {l₁ : list A} (p : [] ~ l₁) : l₁ = [] := have gen : ∀ (l₂ : list A) (p : l₂ ~ l₁), l₂ = [] → l₁ = [], from take l₂ p, perm.induction_on p (λ h, h) - (λ x y l₁ l₂ p₁ r₁, by contradiction) - (λ x y l e, by contradiction) + (by contradiction) + (by contradiction) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ e, r₂ (r₁ e)), gen [] p rfl theorem not_perm_nil_cons (x : A) (l : list A) : ¬ [] ~ (x::l) := have gen : ∀ (l₁ l₂ : list A) (p : l₁ ~ l₂), l₁ = [] → l₂ = (x::l) → false, from take l₁ l₂ p, perm.induction_on p - (λ e₁ e₂, by contradiction) - (λ x l₁ l₂ p₁ r₁ e₁ e₂, by contradiction) - (λ x y l e₁ e₂, by contradiction) + (by contradiction) + (by contradiction) + (by contradiction) (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂ e₁ e₂, begin rewrite [e₂ at *, e₁ at *],