diff options
| author | Andreas Grois <andi@grois.info> | 2025-10-12 18:44:32 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2025-10-12 18:44:32 +0200 |
| commit | 6aaa70943202efaa1e6b4ff8b6b8b6b94a564040 (patch) | |
| tree | 171a1a1b459b82f016e756e8649767a2d1311160 /Common | |
| parent | 2a9261d1ba962deff9fcc1784be44563af513af5 (diff) | |
Lean 4.19
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/List.lean | 6 | ||||
| -rw-r--r-- | Common/Parsing.lean | 2 |
2 files changed, 4 insertions, 4 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 := diff --git a/Common/Parsing.lean b/Common/Parsing.lean index 8237613..7834e00 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -88,7 +88,7 @@ def RectangularGrid.set {grid : RectangularGrid Element} (coordinate : grid.Coor { grid with elements := grid.elements.set index value - size_valid := (grid.elements.size_set index value index.isLt).substr grid.size_valid + size_valid := (grid.elements.size_set index.isLt).substr grid.size_valid } theorem RectangularGrid.set_same_size {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : (grid.set coordinate value).width = grid.width ∧ (grid.set coordinate value).height = grid.height := |