chore: adaptations for nightly-2024-07-30#15358
Conversation
…hlib4 into nightly-testing
…hlib4 into nightly-testing
PR summary d9423736c0
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.String.Lemmas | 18 | 17 | -1 (-5.56%) |
| Mathlib.Data.List.Nodup | 328 | 330 | +2 (+0.61%) |
| Mathlib.Order.Chain | 340 | 342 | +2 (+0.59%) |
| Mathlib.Data.List.Zip | 273 | 274 | +1 (+0.37%) |
| Mathlib.Data.List.Chain | 279 | 280 | +1 (+0.36%) |
| Mathlib.Combinatorics.SimpleGraph.Path | 526 | 527 | +1 (+0.19%) |
| Mathlib.RingTheory.IsTensorProduct | 1136 | 1137 | +1 (+0.09%) |
| Mathlib.AlgebraicGeometry.Properties | 1598 | 1599 | +1 (+0.06%) |
| Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable | 1659 | 1660 | +1 (+0.06%) |
| Mathlib.Probability.ConditionalExpectation | 1718 | 1719 | +1 (+0.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 3913 files with changed transitive imports: this is too many to display! |
Declarations diff
+ _
+ coeMLList
+ exists'
+ 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
- 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'
- 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
- 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»
-++--+- ext
-+-+ Hom.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>
jcommelin
left a comment
There was a problem hiding this comment.
I would like to reset the whitespace changes in certain files.
git checkout bump/v4.11.0 -- Mathlib/Data/Fin/Basic.lean Mathlib/Data/Finsupp/Defs.leanbors d+
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
As it turns out I had already fixed the whitespace on #15282. I've incorporated it here, and hopefully made it stick on |
No description provided.