[Merged by Bors] - chore: adaptations for nightly-2024-07-12#14783
[Merged by Bors] - chore: adaptations for nightly-2024-07-12#14783kim-em wants to merge 4 commits intobump/v4.11.0from
Conversation
PR summary 1ceb6feaae
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.List.GetD | 127 | 103 | -24 (-18.90%) |
| Mathlib.Data.List.Basic | 268 | 266 | -2 (-0.75%) |
| Mathlib.Data.List.Forall2 | 269 | 267 | -2 (-0.74%) |
| Mathlib.Data.List.Join | 269 | 267 | -2 (-0.74%) |
| Mathlib.Data.List.DropRight | 270 | 268 | -2 (-0.74%) |
| Mathlib.Data.List.Chain | 275 | 273 | -2 (-0.73%) |
| Mathlib.Data.List.OfFn | 341 | 339 | -2 (-0.59%) |
| Mathlib.Data.List.Sort | 348 | 346 | -2 (-0.57%) |
| Mathlib.Data.List.Nodup | 323 | 322 | -1 (-0.31%) |
| Mathlib.Data.LazyList.Basic | 354 | 355 | +1 (+0.28%) |
| Mathlib.Algebra.BigOperators.Group.List | 368 | 367 | -1 (-0.27%) |
| Mathlib.Data.Multiset.Basic | 372 | 371 | -1 (-0.27%) |
| Mathlib.Data.Multiset.Nodup | 381 | 380 | -1 (-0.26%) |
| Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc | 404 | 403 | -1 (-0.25%) |
| Mathlib.Data.List.Cycle | 461 | 460 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Limits.VanKampen | 539 | 538 | -1 (-0.19%) |
| Mathlib.Data.Nat.Nth | 591 | 590 | -1 (-0.17%) |
| Mathlib.GroupTheory.CoprodI | 613 | 612 | -1 (-0.16%) |
| Mathlib.Combinatorics.Additive.PluenneckeRuzsa | 745 | 744 | -1 (-0.13%) |
| Mathlib.GroupTheory.Coxeter.Inversion | 904 | 903 | -1 (-0.11%) |
| Mathlib.RingTheory.MaximalSpectrum | 1088 | 1087 | -1 (-0.09%) |
| Mathlib.Algebra.Homology.DerivedCategory.Ext | 1100 | 1099 | -1 (-0.09%) |
| Mathlib.LinearAlgebra.Charpoly.Basic | 1183 | 1182 | -1 (-0.08%) |
| Mathlib.LinearAlgebra.QuadraticForm.Basic | 1186 | 1185 | -1 (-0.08%) |
| Mathlib.Algebra.Category.HopfAlgebraCat.Basic | 1225 | 1224 | -1 (-0.08%) |
Import changes for all files
| Files | Import difference |
|---|---|
| Too many changes (4041)! |
Declarations diff
+ _
+ bind_singleton
+ get_mk
+ get_pure
+ 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?
++++ ext_iff'
- AddContent.ext_iff
- Bornology.ext_iff
- MeasurableSpace.ext_iff
- Mem
- Mem.decidable
- Nodup.erase
- Nodup.erase_eq_filter
- Nodup.mem_erase_iff
- Nodup.not_mem_erase
- Nodup.sublist
- Perm.ext_iff
- Sublist.map
- append_assoc
- append_bind
- append_nil
- attach
- bind
- decidableEq
- eq_iff
- exists_eq_right'
- find
- forall_mem_cons
- forall_mem_ne
- get!_none
- get!_some
- getLast?_append
- getLast_reverse
- head?_append
- head_mem
- head_replicate
- init
- instance : (forget V G).Faithful where map_injective w := Hom.ext _ _ w
- instance : Monad LazyList
- instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ ext_iff
- instance {α} : Membership α (LazyList α)
- instance {α} [Repr α] : Repr (LazyList α)
- interleave
- interleaveAll
- isSome_map
- join_append
- join_concat
- join_reverse
- limit_ext_iff
- mem_cons
- mem_nil
- mfirst
- ne_nil_of_length_pos
- nodup_cons
- nodup_nil
- nodup_replicate
- pi_ext'_iff
- pmap
- reverse
- reverse_join
- sublist_replicate_iff
- takeWhile_cons_of_neg
- takeWhile_cons_of_pos
- traverse
- 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>|
Pull request successfully merged into bump/v4.11.0. Build succeeded: |
No description provided.