From 445cd8f0ae1dd3310017fb5af5e950af3bc4ff7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Nov 2017 21:50:25 -0800 Subject: [PATCH] chore(library/init/data/list/lemmas): ._ ==> _ --- library/init/data/list/lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index 319c60f0a7..eea4ba6425 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -205,9 +205,9 @@ inductive sublist : list α → list α → Prop infix ` <+ `:50 := sublist lemma length_le_of_sublist : ∀ {l₁ l₂ : list α}, l₁ <+ l₂ → length l₁ ≤ length l₂ -| ._ ._ sublist.slnil := le_refl 0 -| ._ ._ (sublist.cons l₁ l₂ a s) := le_succ_of_le (length_le_of_sublist s) -| ._ ._ (sublist.cons2 l₁ l₂ a s) := succ_le_succ (length_le_of_sublist s) +| _ _ sublist.slnil := le_refl 0 +| _ _ (sublist.cons l₁ l₂ a s) := le_succ_of_le (length_le_of_sublist s) +| _ _ (sublist.cons2 l₁ l₂ a s) := succ_le_succ (length_le_of_sublist s) /- filter -/ @[simp] theorem filter_nil (p : α → Prop) [h : decidable_pred p] : filter p [] = [] := rfl