[Merged by Bors] - chore: move toolchain to v4.11.0-rc1#15513
[Merged by Bors] - chore: move toolchain to v4.11.0-rc1#15513
Conversation
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
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>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
PR summary c7bba38e08
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Init.Data.Nat.GCD | 2 | 0 | -2 (-100.00%) |
| Mathlib.Data.List.Enum | 272 | 4 | -268 (-98.53%) |
| Mathlib.Data.List.Count | 272 | 106 | -166 (-61.03%) |
| Mathlib.Lean.Name | 4 | 3 | -1 (-25.00%) |
| Mathlib.Tactic.Linter.Lint | 4 | 3 | -1 (-25.00%) |
| Mathlib.Tactic.Linter.UnusedTactic | 4 | 3 | -1 (-25.00%) |
| Mathlib.Tactic.Attr.Core | 5 | 4 | -1 (-20.00%) |
| Mathlib.Tactic.Widget.Calc | 11 | 13 | +2 (+18.18%) |
| Mathlib.Data.List.GetD | 130 | 108 | -22 (-16.92%) |
| Mathlib.Util.LongNames | 12 | 10 | -2 (-16.67%) |
| Mathlib.Data.List.Intervals | 339 | 297 | -42 (-12.39%) |
| Mathlib.Tactic.Widget.Conv | 11 | 12 | +1 (+9.09%) |
| Mathlib.Data.String.Lemmas | 18 | 17 | -1 (-5.56%) |
| Mathlib.Data.List.Iterate | 430 | 413 | -17 (-3.95%) |
| Mathlib.Order.RelClasses | 136 | 131 | -5 (-3.68%) |
| Mathlib.Data.List.NatAntidiagonal | 337 | 330 | -7 (-2.08%) |
| Mathlib.Logic.Nontrivial.Basic | 100 | 98 | -2 (-2.00%) |
| Mathlib.Data.Sigma.Order | 172 | 169 | -3 (-1.74%) |
| Mathlib.Data.List.Sigma | 346 | 340 | -6 (-1.73%) |
| Mathlib.Data.List.AList | 347 | 341 | -6 (-1.73%) |
| Mathlib.Data.Multiset.Nodup | 388 | 382 | -6 (-1.55%) |
| Mathlib.Data.Multiset.FinsetOps | 390 | 385 | -5 (-1.28%) |
| Mathlib.Data.Finset.Basic | 395 | 390 | -5 (-1.27%) |
| Mathlib.Data.Sigma.Basic | 84 | 83 | -1 (-1.19%) |
| Mathlib.Data.Subtype | 84 | 83 | -1 (-1.19%) |
| Mathlib.Data.Prod.Basic | 87 | 86 | -1 (-1.15%) |
| Mathlib.Data.Option.Basic | 92 | 91 | -1 (-1.09%) |
| Mathlib.Order.RelIso.Basic | 184 | 182 | -2 (-1.09%) |
| Mathlib.Logic.Relation | 93 | 92 | -1 (-1.08%) |
| Mathlib.Data.Set.Basic | 211 | 209 | -2 (-0.95%) |
| Mathlib.Data.PEquiv | 215 | 213 | -2 (-0.93%) |
| Mathlib.Algebra.Ring.Ext | 115 | 114 | -1 (-0.87%) |
| Mathlib.Logic.Equiv.Defs | 117 | 116 | -1 (-0.85%) |
| Mathlib.Combinatorics.Quiver.Basic | 121 | 120 | -1 (-0.83%) |
| Mathlib.Algebra.Group.Units | 137 | 136 | -1 (-0.73%) |
| Mathlib.Data.Set.Pairwise.Basic | 314 | 316 | +2 (+0.64%) |
| Mathlib.Tactic.Abel | 350 | 352 | +2 (+0.57%) |
| Mathlib.Algebra.Group.Equiv.Basic | 178 | 179 | +1 (+0.56%) |
| Mathlib.Algebra.Order.Monoid.Unbundled.Basic | 178 | 177 | -1 (-0.56%) |
| Mathlib.GroupTheory.Congruence.Basic | 372 | 374 | +2 (+0.54%) |
| Mathlib.Algebra.Ring.Hom.Defs | 190 | 191 | +1 (+0.53%) |
| Mathlib.CategoryTheory.Limits.Shapes.Types | 426 | 428 | +2 (+0.47%) |
| Mathlib.Data.NNRat.Defs | 457 | 459 | +2 (+0.44%) |
| Mathlib.Data.List.Join | 273 | 272 | -1 (-0.37%) |
| Mathlib.Data.Complex.Basic | 553 | 555 | +2 (+0.36%) |
| Mathlib.Data.Seq.Seq | 279 | 278 | -1 (-0.36%) |
| Mathlib.CategoryTheory.Bicategory.LocallyDiscrete | 302 | 303 | +1 (+0.33%) |
| Mathlib.Algebra.Free | 304 | 305 | +1 (+0.33%) |
| Mathlib.CategoryTheory.Bicategory.Coherence | 308 | 309 | +1 (+0.32%) |
| Mathlib.CategoryTheory.Yoneda | 308 | 309 | +1 (+0.32%) |
| Mathlib.Data.List.Nodup | 328 | 329 | +1 (+0.30%) |
| Mathlib.CategoryTheory.IsConnected | 335 | 336 | +1 (+0.30%) |
| Mathlib.Data.List.OfFn | 335 | 334 | -1 (-0.30%) |
| Mathlib.Data.List.Range | 336 | 335 | -1 (-0.30%) |
| Mathlib.CategoryTheory.ConnectedComponents | 337 | 338 | +1 (+0.30%) |
| Mathlib.Data.List.Sublists | 347 | 346 | -1 (-0.29%) |
| Mathlib.Data.List.Indexes | 348 | 347 | -1 (-0.29%) |
| Mathlib.CategoryTheory.Monoidal.NaturalTransformation | 371 | 372 | +1 (+0.27%) |
| Mathlib.SetTheory.ZFC.Basic | 372 | 371 | -1 (-0.27%) |
| Mathlib.CategoryTheory.Monoidal.Free.Coherence | 373 | 374 | +1 (+0.27%) |
| Mathlib.Algebra.BigOperators.Group.List | 374 | 373 | -1 (-0.27%) |
| Mathlib.CategoryTheory.Category.PartialFun | 374 | 375 | +1 (+0.27%) |
| Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy | 374 | 375 | +1 (+0.27%) |
| Mathlib.Algebra.Module.Defs | 381 | 382 | +1 (+0.26%) |
| Mathlib.Algebra.Order.BigOperators.Group.List | 384 | 383 | -1 (-0.26%) |
| Mathlib.CategoryTheory.Endofunctor.Algebra | 384 | 385 | +1 (+0.26%) |
| Mathlib.GroupTheory.SemidirectProduct | 384 | 385 | +1 (+0.26%) |
| Mathlib.GroupTheory.GroupAction.Hom | 385 | 386 | +1 (+0.26%) |
| Mathlib.Data.Vector.Zip | 389 | 388 | -1 (-0.26%) |
| Mathlib.CategoryTheory.Localization.Resolution | 390 | 391 | +1 (+0.26%) |
| Mathlib.CategoryTheory.Monoidal.Braided.Basic | 396 | 397 | +1 (+0.25%) |
| Mathlib.Algebra.Module.LinearMap.Defs | 397 | 398 | +1 (+0.25%) |
| Mathlib.Algebra.Module.Equiv.Defs | 398 | 399 | +1 (+0.25%) |
| Mathlib.CategoryTheory.Comma.StructuredArrow | 400 | 401 | +1 (+0.25%) |
| Mathlib.CategoryTheory.Grothendieck | 403 | 404 | +1 (+0.25%) |
| Mathlib.CategoryTheory.Comma.Presheaf | 404 | 405 | +1 (+0.25%) |
| Mathlib.Algebra.Star.StarRingHom | 405 | 406 | +1 (+0.25%) |
| Mathlib.CategoryTheory.Sites.Sieves | 407 | 408 | +1 (+0.25%) |
| Mathlib.CategoryTheory.Limits.Shapes.Images | 412 | 413 | +1 (+0.24%) |
| Mathlib.CategoryTheory.Limits.Types | 414 | 415 | +1 (+0.24%) |
| Mathlib.CategoryTheory.Limits.Preserves.Ulift | 417 | 418 | +1 (+0.24%) |
| Mathlib.Data.Sym.Basic | 418 | 417 | -1 (-0.24%) |
| Mathlib.Testing.SlimCheck.Testable | 419 | 420 | +1 (+0.24%) |
| Mathlib.CategoryTheory.Monoidal.Rigid.Basic | 420 | 421 | +1 (+0.24%) |
| Mathlib.Algebra.Homology.ShortComplex.Basic | 421 | 422 | +1 (+0.24%) |
| Mathlib.CategoryTheory.Sites.Pretopology | 422 | 423 | +1 (+0.24%) |
| Mathlib.CategoryTheory.Sites.SheafOfTypes | 426 | 427 | +1 (+0.23%) |
| Mathlib.CategoryTheory.Subobject.Basic | 426 | 427 | +1 (+0.23%) |
| Mathlib.CategoryTheory.Shift.SingleFunctors | 433 | 434 | +1 (+0.23%) |
| Mathlib.CategoryTheory.DifferentialObject | 435 | 436 | +1 (+0.23%) |
| Mathlib.Data.List.Sym | 439 | 438 | -1 (-0.23%) |
| Mathlib.Data.Finmap | 461 | 460 | -1 (-0.22%) |
| Mathlib.CategoryTheory.Monoidal.Mon_ | 468 | 469 | +1 (+0.21%) |
| Mathlib.CategoryTheory.Monoidal.CommMon_ | 469 | 470 | +1 (+0.21%) |
| Mathlib.CategoryTheory.Monoidal.Mod_ | 469 | 470 | +1 (+0.21%) |
| Mathlib.Algebra.CharP.Defs | 470 | 471 | +1 (+0.21%) |
| Mathlib.CategoryTheory.Monoidal.Comon_ | 471 | 472 | +1 (+0.21%) |
| Mathlib.CategoryTheory.Monoidal.Bimon_ | 472 | 473 | +1 (+0.21%) |
| Mathlib.CategoryTheory.Monoidal.Bimod | 474 | 475 | +1 (+0.21%) |
| Mathlib.CategoryTheory.Filtered.Small | 513 | 512 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Limits.Shapes.Biproducts | 525 | 524 | -1 (-0.19%) |
| Mathlib.Computability.Primrec | 531 | 530 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Dialectica.Basic | 533 | 532 | -1 (-0.19%) |
| Mathlib.CategoryTheory.GradedObject.Monoidal | 535 | 534 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Triangulated.Basic | 537 | 536 | -1 (-0.19%) |
| Mathlib.CategoryTheory.GuitartExact.Basic | 538 | 537 | -1 (-0.19%) |
| Mathlib.CategoryTheory.Monad.Coequalizer | 546 | 545 | -1 (-0.18%) |
| Mathlib.CategoryTheory.Monad.Equalizer | 546 | 545 | -1 (-0.18%) |
| Mathlib.RepresentationTheory.Action.Basic | 547 | 546 | -1 (-0.18%) |
| Mathlib.CategoryTheory.Limits.VanKampen | 552 | 551 | -1 (-0.18%) |
| Mathlib.NumberTheory.Pell | 1407 | 1406 | -1 (-0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 1166 files with changed transitive imports: this is too many to display! |
Declarations diff
+ _
+ adj_sndOfNotNil
+ coeMLList
+ cons_getVert
+ cons_getVert_succ
+ cons_sndOfNotNil
+ exists'
+ ext_iff'
+ filter_subset'
+ getVert_one
+ 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
+ sndOfNotNil
+ tail_support_eq_support_tail
+ 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
- adj_getVert_one
- and_forall_succ
- attach_eq_nil
- attach_map_val
- attach_nil
- countP_attach
- count_attach
- drop
- 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'
- exists_prop_congr
- exists_prop_of_true
- exists_true_left
- 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
- getVert_cons
- getVert_cons_one
- getVert_cons_succ
- getVert_copy
- 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
- not_nil_iff_lt_length
- or_exists_succ
- 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
- support_tail_of_not_nil
- tail_cons_eq
- tail_cons_nil
- 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»
-+-+ Hom.ext'
-+-+- 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>The doc-module for script/declarations_diff.sh contains some details about this script.
|
As this PR is labelled bors merge |
|
bors p=10 |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
No description provided.