[Merged by Bors] - chore: adaptations for nightly-2024-07-31#15366
[Merged by Bors] - chore: adaptations for nightly-2024-07-31#15366kim-em wants to merge 1415 commits intobump/v4.11.0from
Conversation
PR summary 5f4fbe4b99
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Order.Chain | 340 | 342 | +2 (+0.59%) |
| Mathlib.Data.Fin.Basic | 319 | 320 | +1 (+0.31%) |
| Mathlib.Data.Finmap | 461 | 460 | -1 (-0.22%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 1165 files with changed transitive imports: this is too many to display! |
Declarations diff
+ _
+ coeMLList
+ exists'
+ ext_iff'
+ filter_subset'
+ instance : (forget V G).Faithful where map_injective w := Hom.ext w
+ mem_getLast?_append_of_mem_getLast?
+ mem_head?_append_of_mem_head?
+ ofMLList
+ toLazyList
+-+- empty_toList
- AddContent.ext_iff
- Bornology.ext_iff
- MeasurableSpace.ext_iff
- Nodup.erase
- Nodup.erase_eq_filter
- Nodup.mem_erase_iff
- Nodup.not_mem_erase
- Nodup.sublist
- Perm.ext_iff
- Sublist.map
- TransGen
- _root_.Acc.TransGen
- _root_.WellFounded.transGen
- _root_.acc_transGen_iff
- and_forall_succ
- attach_eq_nil
- attach_map_val
- attach_nil
- countP_attach
- count_attach
- enumFrom_append
- enumFrom_cons'
- enumFrom_eq_nil
- enumFrom_eq_zip_range'
- enumFrom_map
- enumFrom_map_snd
- enumFrom_singleton
- enum_append
- enum_cons'
- enum_eq_nil
- enum_eq_zip_range
- enum_map
- enum_map_snd
- enum_singleton
- eq_iff
- exists_eq_right'
- exists_or_eq_left
- exists_or_eq_left'
- exists_or_eq_right
- exists_or_eq_right'
- exists_prop_congr
- exists_prop_of_true
- exists_true_left
- ext_dual_iff
- ext_inner_iff
- filter_subset
- foldl_join
- foldr_join
- forall_mem_ne
- fst_lt_add_of_mem_enumFrom
- fst_lt_of_mem_enum
- gcd_def
- get!_none
- get!_some
- get?_pmap
- getElem?_enum
- getElem?_enumFrom
- getElem?_pmap
- getElem?_zipWith'
- getElem?_zipWith_eq_some
- getElem?_zip_eq_some
- getElem_enum
- getElem_enumFrom
- getElem_eq_getElem?
- getElem_pmap
- getElem_zip
- getElem_zipWith
- getLast?_append
- getLast_cons
- getLast_pmap
- getLast_reverse
- get_pmap
- head?_append
- head_mem
- head_replicate
- instance : (forget V G).Faithful where map_injective w := Hom.ext _ _ w
- isSome_map
- join_append
- join_concat
- join_join
- join_reverse
- le_fst_of_mem_enumFrom
- length_attach
- length_filter_lt_length_iff_exists
- length_join
- length_pmap
- limit_ext_iff
- lt_length_left_of_zip
- lt_length_left_of_zipWith
- lt_length_right_of_zip
- lt_length_right_of_zipWith
- map_eq_map_iff
- map_fst_add_enumFrom_eq_enumFrom
- map_fst_add_enum_eq_enumFrom
- map_pmap
- map_prod_left_eq_zip
- map_prod_right_eq_zip
- mem_attach
- mem_enumFrom
- mem_pmap
- mem_zip
- ne_nil_of_length_pos
- nodup_cons
- nodup_iota
- nodup_nil
- nodup_range
- nodup_range'
- nodup_replicate
- or_exists_succ
- pairwise_gt_iota
- pairwise_le_range
- pairwise_lt_range
- pairwise_lt_range'
- pi_ext'_iff
- pmap_append
- pmap_append'
- pmap_congr
- pmap_eq_map
- pmap_eq_map_attach
- pmap_eq_nil
- pmap_map
- range'_one
- reverse_eq_iff
- reverse_join
- snd_mem_of_mem_enum
- snd_mem_of_mem_enumFrom
- sublist_replicate_iff
- takeWhile_cons_of_neg
- takeWhile_cons_of_pos
- take_range
- unique_ext_iff
- unzip_enumFrom_eq_prod
- unzip_enum_eq_prod
- unzip_eq_map
- unzip_left
- unzip_right
- unzip_zip
- unzip_zip_left
- unzip_zip_right
- zipWith_comm
- zipWith_comm_of_comm
- zipWith_distrib_reverse
- zipWith_same
- zip_of_prod
- zip_unzip
- «forall»
-+-+ Hom.ext'
-+-+- ext
-- subtype_ext_iff
-- «exists»
--- ext_ring_iff
------------------------------------------------------------------------------------------------------------ ext_iff
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
| ### order | ||
| -/ | ||
|
|
||
|
|
There was a problem hiding this comment.
(These whitespace changes make bump/v4.11.0 match master, so should be kept)
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
|
bors merge |
|
Already running a review |
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
|
Pull request successfully merged into bump/v4.11.0. Build succeeded: |
No description provided.