From 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 12 Oct 2025 18:44:32 +0200
Subject: Lean 4.19

---
 Common/List.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Common/List.lean')

diff --git a/Common/List.lean b/Common/List.lean
index 1c8f4a6..f6c0de5 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -54,7 +54,7 @@ instance {α : Type} [Ord α] : Ord (List α) where
 def not_empty_iff_size_gt_zero {list : List α} : list.isEmpty = false ↔ list.length > 0 :=
   match list with
   | [] => ⟨nofun, nofun⟩
-  | l :: ls => ⟨λ_ ↦ (List.length_cons l ls).substr (Nat.succ_pos ls.length), λ_ => rfl⟩
+  | _l :: ls => ⟨λ_ ↦ (List.length_cons).substr (Nat.succ_pos ls.length), λ_ => rfl⟩
 
 def ne_nil_of_not_empty {list : List α} : list.isEmpty = false ↔ list ≠ [] :=
   match list with
@@ -79,14 +79,14 @@ where
   | [], _, bs => bs.reverse
   | a :: as, f, bs =>
     let g : (e : α) → (e ∈ as) → β := λ e h ↦ f e (List.mem_cons_of_mem a h)
-    worker as g (f a (List.mem_cons_self _ _) :: bs)
+    worker as g (f a (List.mem_cons_self) :: bs)
 
 protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : List α) (f : (e : α) → (e ∈ list) → β) (acc : List β) : list.length + acc.length = (List.mapWithProof.worker list f acc).length := by
   induction list generalizing acc
   case nil => unfold mapWithProof.worker; simp only [length_nil, Nat.zero_add, length_reverse]
   case cons l ls hi =>
     unfold mapWithProof.worker
-    have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self _ _) :: acc)
+    have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self) :: acc)
     simp +arith[←hi]
 
 theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length :=
-- 
cgit v1.2.3

