Skip to content

[Merged by Bors] - chore: adaptations for nightly-2024-07-17#14846

Closed
kim-em wants to merge 2 commits intobump/v4.11.0from
bump/nightly-2024-07-17
Closed

[Merged by Bors] - chore: adaptations for nightly-2024-07-17#14846
kim-em wants to merge 2 commits intobump/v4.11.0from
bump/nightly-2024-07-17

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Jul 17, 2024 •
edited by mathlib-bors bot
Loading

No description provided.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 17, 2024 •
edited
Loading

PR summary c7c11b6fda

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Order.RelClasses 135 129 -6 (-4.44%)
Mathlib.Algebra.Order.Monoid.Unbundled.Basic 176 174 -2 (-1.14%)
Mathlib.Logic.Relation 95 94 -1 (-1.05%)
Mathlib.Data.Set.Image 215 214 -1 (-0.47%)
Mathlib.CategoryTheory.Limits.Shapes.Types 420 419 -1 (-0.24%)
Mathlib.Data.Finmap 453 452 -1 (-0.22%)
Mathlib.LinearAlgebra.AffineSpace.AffineSubspace 751 750 -1 (-0.13%)
Import changes for all files
Files Import difference
Too many changes (4273)!

Declarations diff

+ _
+ 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?
- 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'
- 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>

@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Jul 18, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 18, 2024
@kim-em
chore: adaptations for nightly-2024-07-17 (#14846)
7625d2b
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 18, 2024

Pull request successfully merged into bump/v4.11.0.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: adaptations for nightly-2024-07-17 [Merged by Bors] - chore: adaptations for nightly-2024-07-17 Jul 18, 2024
@mathlib-bors mathlib-bors bot closed this Jul 18, 2024
@mathlib-bors mathlib-bors bot deleted the bump/nightly-2024-07-17 branch July 18, 2024 08:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kim-em @fpvandoorn