[Merged by Bors] - chore: adaptations for nightly-2024-07-25#15147
[Merged by Bors] - chore: adaptations for nightly-2024-07-25#15147kim-em wants to merge 1313 commits intobump/v4.11.0from
Conversation
…hlib4 into nightly-testing
PR summary 000726f07c
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Seq.Seq | 278 | 276 | -2 (-0.72%) |
| Mathlib.Data.LazyList.Basic | 360 | 359 | -1 (-0.28%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 834 files with changed transitive imports: this is too many to display! |
Declarations diff
+ _
+ coeMLList
+ instance : (forget V G).Faithful where map_injective w := Hom.ext w
+ instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ Units.ext_iff
+ mem_getLast?_append_of_mem_getLast?
+ mem_head?_append_of_mem_head?
+ ofMLList
+ toLazyList
- 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
- 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
- forall_mem_ne
- get!_none
- get!_some
- getLast?_append
- getLast_reverse
- head?_append
- head_mem
- head_replicate
- instance : (forget V G).Faithful where map_injective w := Hom.ext _ _ w
- instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ ext_iff
- isSome_map
- join_append
- join_concat
- join_reverse
- limit_ext_iff
- ne_nil_of_length_pos
- nodup_cons
- nodup_nil
- nodup_replicate
- pi_ext'_iff
- reverse_join
- sublist_replicate_iff
- takeWhile_cons_of_neg
- takeWhile_cons_of_pos
- unique_ext_iff
-++-+- ext
-+-+ Hom.ext'
-- subtype_ext_iff
--- 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>|
Looks fine to me. bors merge |
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
|
Pull request successfully merged into bump/v4.11.0. Build succeeded: |
No description provided.