chore(data/list): drop list.is_nil (#7269)

We have `list.empty` in Lean core.

src/data/list/basic.lean

@@ -614,10 +614,12 @@ by induction l; [refl, simp only [*, reverse_cons, mem_append, mem_singleton, me
 eq_repeat.2 ⟨by simp only [length_reverse, length_repeat],
   λ b h, eq_of_mem_repeat (mem_reverse.1 h)⟩
 
-/-! ### is_nil -/
+/-! ### empty -/
 
-lemma is_nil_iff_eq_nil {l : list α} : l.is_nil ↔ l = [] :=
-list.cases_on l (by simp [is_nil]) (by simp [is_nil])
+attribute [simp] list.empty
+
+lemma empty_iff_eq_nil {l : list α} : l.empty ↔ l = [] :=
+list.cases_on l (by simp) (by simp)
 
 /-! ### init -/
 

src/data/list/defs.lean

@@ -19,11 +19,6 @@ open function nat native (rb_map mk_rb_map rb_map.of_list)
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
-/-- Returns whether a list is []. Returns a boolean even if `l = []` is not decidable. -/
-def is_nil {α} : list α → bool
-| [] := tt
-| _  := ff
-
 instance [decidable_eq α] : has_sdiff (list α) :=
 ⟨ list.diff ⟩