chore: adaptations for nightly-2024-07-26#15181
Conversation
…leanprover-community/mathlib4 into nightly-testing
PR summary 1db04a5f2e
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.Linter.Lint | 4 | 3 | -1 (-25.00%) |
| Mathlib.Data.List.Join | 273 | 271 | -2 (-0.73%) |
| Mathlib.Data.List.Basic | 271 | 270 | -1 (-0.37%) |
| Mathlib.Data.List.Lattice | 272 | 271 | -1 (-0.37%) |
| Mathlib.Data.List.DropRight | 273 | 272 | -1 (-0.37%) |
| Mathlib.Data.List.Destutter | 280 | 279 | -1 (-0.36%) |
| Mathlib.Data.List.Perm | 338 | 337 | -1 (-0.30%) |
| Mathlib.Data.Multiset.Basic | 379 | 378 | -1 (-0.26%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 828 files with changed transitive imports: this is too many to display! |
Declarations diff
+ _
+ coeMLList
+ filter_subset'
+ 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
+-+- 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
- 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
- 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_join
- join_reverse
- length_join
- limit_ext_iff
- map_eq_map_iff
- ne_nil_of_length_pos
- nodup_cons
- nodup_nil
- nodup_replicate
- pi_ext'_iff
- reverse_eq_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>|
bors d+ |
|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
No description provided.