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

chore: minor improvements (#9708)

Browse source 
This PR stylistically improves an internal hash map proof and fixes a
typo in the docsting of `String.join`.
This commit is contained in:
Markus Himmel 2025-08-04 09:12:05 +02:00 • committed by GitHub
parent c260435913
commit 3eab35ef22
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 16 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/String/Basic.lean
View file

@ -652,7 +652,7 @@ Use `String.intercalate` to place a separator string between the strings in a li
Examples:
* `String.join ["gr", "ee", "n"] = "green"`
* `String.join ["b", "", "l", "", "ue"] = "red"`
* `String.join ["b", "", "l", "", "ue"] = "blue"`
* `String.join [] = ""`
-/
@[inline] def join (l : List String) : String :=

30
src/Std/Data/DHashMap/Internal/WF.lean
View file

@ -1009,21 +1009,21 @@ namespace Raw
theorem WF.out [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashable α] {m : Raw α β}
(h : m.WF) : Raw.WFImp m := by
induction h generalizing i₁ i₂
next h => apply h
· exact Raw₀.wfImp_emptyWithCapacity
next h => exact Raw₀.wfImp_insert (by apply h)
next h => exact Raw₀.wfImp_containsThenInsert (by apply h)
next h => exact Raw₀.wfImp_containsThenInsertIfNew (by apply h)
next h => exact Raw₀.wfImp_erase (by apply h)
next h => exact Raw₀.wfImp_insertIfNew (by apply h)
next h => exact Raw₀.wfImp_getThenInsertIfNew? (by apply h)
next h => exact Raw₀.wfImp_filter (by apply h)
next h => exact Raw₀.Const.wfImp_getThenInsertIfNew? (by apply h)
next h => exact Raw₀.wfImp_modify (by apply h)
next h => exact Raw₀.Const.wfImp_modify (by apply h)
next h => exact Raw₀.wfImp_alter (by apply h)
next h => exact Raw₀.Const.wfImp_alter (by apply h)
induction h generalizing i₁ i₂ with
| wf _ h => apply h
| emptyWithCapacity₀ => exact Raw₀.wfImp_emptyWithCapacity
| insert₀ _ h => exact Raw₀.wfImp_insert (by apply h)
| containsThenInsert₀ _ h => exact Raw₀.wfImp_containsThenInsert (by apply h)
| containsThenInsertIfNew₀ _ h => exact Raw₀.wfImp_containsThenInsertIfNew (by apply h)
| erase₀ _ h => exact Raw₀.wfImp_erase (by apply h)
| insertIfNew₀ _ h => exact Raw₀.wfImp_insertIfNew (by apply h)
| getThenInsertIfNew?₀ _ h => exact Raw₀.wfImp_getThenInsertIfNew? (by apply h)
| filter₀ _ h => exact Raw₀.wfImp_filter (by apply h)
| constGetThenInsertIfNew?₀ _ h => exact Raw₀.Const.wfImp_getThenInsertIfNew? (by apply h)
| modify₀ _ h => exact Raw₀.wfImp_modify (by apply h)
| constModify₀ _ h => exact Raw₀.Const.wfImp_modify (by apply h)
| alter₀ _ h => exact Raw₀.wfImp_alter (by apply h)
| constAlter₀ _ h => exact Raw₀.Const.wfImp_alter (by apply h)
end Raw