max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: List.modifyTailIdx naming fix (#6007)

Browse source
This commit is contained in:
Kim Morrison 2024-11-08 13:42:06 +11:00 • committed by GitHub
parent 1b806c5535
commit 680177049f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/List/Nat/InsertIdx.lean
View file

@ -53,7 +53,7 @@ theorem length_insertIdx_of_length_lt (h : length as < n) : length (insertIdx n
simp [length_insertIdx, h]
theorem eraseIdx_insertIdx (n : Nat) (l : List α) : (l.insertIdx n a).eraseIdx n = l := by
rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_eq]
rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
exact modifyTailIdx_id _ _
theorem insertIdx_eraseIdx_of_ge :

2
src/Init/Data/List/Nat/Modify.lean
View file

@ -125,7 +125,7 @@ theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (m n : Nat) (
rcases Nat.exists_eq_add_of_le h with ⟨m, rfl⟩
rw [Nat.add_comm, modifyTailIdx_modifyTailIdx, Nat.add_sub_cancel]
theorem modifyTailIdx_modifyTailIdx_eq {f g : List α → List α} (n : Nat) (l : List α) :
theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (n : Nat) (l : List α) :
(l.modifyTailIdx f n).modifyTailIdx g n = l.modifyTailIdx (g ∘ f) n := by
rw [modifyTailIdx_modifyTailIdx_le n n l (Nat.le_refl n), Nat.sub_self]; rfl