From 5ae63ea1f255c32faef24fce152aeae23962683e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Sep 2018 17:10:23 -0700 Subject: [PATCH] chore(library/init/data/list/basic): remove unnecessary workaround --- library/init/data/list/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index c9cdf44e70..d323dbbb91 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -154,7 +154,7 @@ def find_index (p : α → Prop) [decidable_pred p] : list α → nat | (a::l) := if p a then 0 else succ (find_index l) def index_of [decidable_eq α] (a : α) (l : list α) : nat := -@find_index _ (eq a) (dec_eq a) l +find_index (eq a) l def assoc [decidable_eq α] : list (α × β) → α → option β | [] _ := none