diff options
Diffstat (limited to 'Common/List.lean')
| -rw-r--r-- | Common/List.lean | 6 |
1 files changed, 3 insertions, 3 deletions
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 := |