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

chore: fix name of List.length_mergeSort (#5373)

Browse source
This commit is contained in:
Kim Morrison 2024-09-17 22:43:39 +10:00 • committed by GitHub
parent b74f85accd
commit 21d71de481
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/List/Sort/Lemmas.lean
View file

@ -234,7 +234,7 @@ theorem mergeSort_perm : ∀ (l : List α) (le), mergeSort l le ~ l
(Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))
termination_by l => l.length
@[simp] theorem mergeSort_length (l : List α) : (mergeSort l le).length = l.length :=
@[simp] theorem length_mergeSort (l : List α) : (mergeSort l le).length = l.length :=
(mergeSort_perm l le).length_eq
@[simp] theorem mem_mergeSort {a : α} {l : List α} : a ∈ mergeSort l le ↔ a ∈ l :=