From 018f76855570cd4635109783a0f754a9a6fa2b6d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Apr 2015 14:39:59 -0700 Subject: [PATCH] chore(library): remove some unnecessary parentheses --- library/algebra/ordered_group.lean | 2 +- library/data/examples/notencodable.lean | 10 +++++----- library/data/int/basic.lean | 4 ++-- library/data/list/comb.lean | 8 ++++---- library/data/list/perm.lean | 24 ++++++++++++------------ library/init/funext.lean | 2 +- 6 files changed, 25 insertions(+), 25 deletions(-) diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index d64ababbf..b5298e20d 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -520,7 +520,7 @@ section have H3 : abs (b + a) ≤ abs b + abs a, begin rewrite add.comm at H1, - exact (aux1 H1 H2) + exact aux1 H1 H2 end, rewrite [add.comm, {abs a + _}add.comm], exact H3 diff --git a/library/data/examples/notencodable.lean b/library/data/examples/notencodable.lean index 55ba37087..e1397f5cc 100644 --- a/library/data/examples/notencodable.lean +++ b/library/data/examples/notencodable.lean @@ -32,11 +32,11 @@ private definition v : nat := encode_fun f private lemma f_eq : succ (f v) = f v := begin - change (succ (f v) = - match decode_fun (encode_fun f) with - | some g := succ (g v) - | none := 0 - end), + change succ (f v) = + match decode_fun (encode_fun f) with + | some g := succ (g v) + | none := 0 + end, rewrite encodek_fun end end diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 1e5025e5a..02467860e 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -372,7 +372,7 @@ begin apply equiv.trans, apply repr_add, apply equiv.symm, - apply (eq.subst (padd_comm (repr b) (repr a))), + apply eq.subst (padd_comm (repr b) (repr a)), apply repr_add end @@ -385,7 +385,7 @@ begin apply eq_of_repr_equiv_repr, apply equiv.trans, apply H1, - apply (eq.subst ((padd_assoc _ _ _)⁻¹)), + apply eq.subst (padd_assoc _ _ _)⁻¹, apply equiv.symm, apply H2 end diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index 0c30467a6..aca5408e7 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -135,9 +135,9 @@ section foldl_eq_foldr | a b nil := Hcomm a b | a b (c::l) := begin - change (foldl f (f (f a b) c) l = f b (foldl f (f a c) l)), + change foldl f (f (f a b) c) l = f b (foldl f (f a c) l), rewrite -foldl_eq_of_comm_of_assoc, - change (foldl f (f (f a b) c) l = foldl f (f (f a c) b) l), + change foldl f (f (f a b) c) l = foldl f (f (f a c) b) l, have H₁ : f (f a b) c = f (f a c) b, by rewrite [Hassoc, Hassoc, Hcomm b c], rewrite H₁ end @@ -148,7 +148,7 @@ section foldl_eq_foldr begin rewrite foldl_eq_of_comm_of_assoc, esimp, - change (f b (foldl f a l) = f b (foldr f a l)), + change f b (foldl f a l) = f b (foldr f a l), rewrite foldl_eq_foldr end end foldl_eq_foldr @@ -259,7 +259,7 @@ theorem zip_unzip : ∀ (l : list (A × B)), zip (pr₁ (unzip l)) (pr₂ (unzip rewrite unzip_cons, have r : zip (pr₁ (unzip l)) (pr₂ (unzip l)) = l, from zip_unzip l, revert r, - apply (prod.cases_on (unzip l)), + apply prod.cases_on (unzip l), intros [la, lb, r], rewrite -r end diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index 3b3a6b9d2..188d0cd4d 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -270,9 +270,9 @@ match l₂ with | [] := λ e h₁ h₂, list.no_confusion e (λ e₁ e₂, h₁ rfl e₁ e₂) | h::t := λ e h₁ h₂, begin - apply (list.no_confusion e), intros [e₁, e₂], + apply list.no_confusion e, intros [e₁, e₂], rewrite e₁ at h₂, - exact (h₂ t rfl e₂) + exact h₂ t rfl e₂ end end @@ -289,17 +289,17 @@ match l₂ with | [h₁] := λ e H₁ H₂ H₃, begin rewrite [append_cons at e, append_nil_left at e], - apply (list.no_confusion e), intros [a_eq_h₁, rest], - apply (list.no_confusion rest), intros [b_eq_c, l₁_eq_l₃], + apply list.no_confusion e, intros [a_eq_h₁, rest], + apply list.no_confusion rest, intros [b_eq_c, l₁_eq_l₃], rewrite [a_eq_h₁ at H₂, b_eq_c at H₂, l₁_eq_l₃ at H₂], - exact (H₂ rfl rfl rfl) + exact H₂ rfl rfl rfl end | h₁::h₂::t₂ := λ e H₁ H₂ H₃, begin - apply (list.no_confusion e), intros [a_eq_h₁, rest], - apply (list.no_confusion rest), intros [b_eq_h₂, l₁_eq], + apply list.no_confusion e, intros [a_eq_h₁, rest], + apply list.no_confusion rest, intros [b_eq_h₂, l₁_eq], rewrite [a_eq_h₁ at H₃, b_eq_h₂ at H₃], - exact (H₃ t₂ rfl l₁_eq) + exact H₃ t₂ rfl l₁_eq end end @@ -546,7 +546,7 @@ assume p, perm_induction_on p begin rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_mem yinxt₂, erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_not_mem nxint₂, xeqy], - exact (skip y r) + exact skip y r end) (λ xney : x ≠ y, have xint₁ : x ∈ t₁, from or_resolve_right xinyt₁ xney, @@ -558,7 +558,7 @@ assume p, perm_induction_on p begin rewrite [erase_dup_cons_of_mem xinyt₁, erase_dup_cons_of_not_mem nyinxt₂, erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_mem xint₂], - exact (skip y r) + exact skip y r end))) (λ nxinyt₁ : x ∉ y::t₁, have xney : x ≠ y, from not_eq_of_not_mem nxinyt₁, @@ -571,7 +571,7 @@ assume p, perm_induction_on p begin rewrite [erase_dup_cons_of_not_mem nxinyt₁, erase_dup_cons_of_mem yinxt₂, erase_dup_cons_of_mem yint₁, erase_dup_cons_of_not_mem nxint₂], - exact (skip x r) + exact skip x r end) (λ nyint₁ : y ∉ t₁, assert nyinxt₂ : y ∉ x::t₂, from @@ -581,7 +581,7 @@ assume p, perm_induction_on p begin rewrite [erase_dup_cons_of_not_mem nxinyt₁, erase_dup_cons_of_not_mem nyinxt₂, erase_dup_cons_of_not_mem nyint₁, erase_dup_cons_of_not_mem nxint₂], - exact (xswap x y r) + exact xswap x y r end))) (λ t₁ t₂ t₃ p₁ p₂ r₁ r₂, trans r₁ r₂) diff --git a/library/init/funext.lean b/library/init/funext.lean index dfa3dc1fa..ea2c4e1c7 100644 --- a/library/init/funext.lean +++ b/library/init/funext.lean @@ -55,7 +55,7 @@ section assume H, calc f₁ = extfun_app ⟦f₁⟧ : rfl ... = extfun_app ⟦f₂⟧ : {sound H} - ... = f₂ : rfl + ... = f₂ : rfl end open function.equiv_notation