[Merged by Bors] - chore: smile more often by eric-wieser · Pull Request #20436 · leanprover-community/mathlib4

eric-wieser · 2025-01-03T13:38:35Z

This replaces : _) with the shorter and otherwise almost identical :). The former is a Lean 3 ism; or at least, the latter is new syntax in Lean 4.

More precisely (thanks @kmill):

(e : _) elaborates e without an expected type, and then it inserts a coercion if the type of e does not match the expected type.
(e :) elaborates e without an expected type to completion, and then it inserts a coercion if the type of e does not match the expected type.

A few places break when switched to :); in many of these cases, the : _)/:) can just be dropped entirely.
The remainder are left as is.

github-actions · 2025-01-03T13:39:30Z

PR summary a75a5a8a48

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ instance : NormedSpace 𝕜 C₀(α, β) where norm_smul_le k f := (norm_smul_le k f.toBCF :)
- instance : NormedSpace 𝕜 C₀(α, β) where norm_smul_le k f := (norm_smul_le k f.toBCF : _)
-+-+-+ this

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

`(e : _)` means something unrelated in binders.

eric-wieser · 2025-01-04T00:37:58Z

!bench

leanprover-bot · 2025-01-04T01:06:35Z

Here are the benchmark results for commit 3b93321.
There were no significant changes against commit 7bbc345.

eric-wieser · 2025-01-07T01:19:12Z

@kmill, can you confirm that this change is actually reasonable, if perhaps a bit of a waste of time?

kmill · 2025-01-07T01:53:54Z

It seems that (e :) isn't less efficient than (e : _), so why not (where it works). Let's smile rather than smirk.

Details:

(e : _) elaborates e without an expected type, and then it inserts a coercion if the type of e does not match the expected type.
(e :) elaborates e without an expected type to completion, and then it inserts a coercion if the type of e does not match the expected type.

eric-wieser · 2025-01-07T01:59:06Z

Thanks, I've stolen that wording for the commit message.

adomani · 2025-01-07T07:29:35Z

:) let's get the smileys in!

bors r+

@kmill

This replaces `: _)` with the shorter and otherwise *almost* identical `:)`. The former is a Lean 3 ism; or at least, the latter is new syntax in Lean 4. More precisely (thanks @kmill): - `(e : _)` elaborates `e` without an expected type, and then it inserts a coercion if the type of `e` does not match the expected type. - `(e :)` elaborates `e` without an expected type *to completion*, and then it inserts a coercion if the type of `e` does not match the expected type. A few places break when switched to `:)`; in many of these cases, the `: _)`/`:)` can just be dropped entirely. The remainder are left as is.

adomani · 2025-01-07T07:30:12Z

Oh, I missed the conflict.

bors d+

mathlib-bors · 2025-01-07T07:30:14Z

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

kbuzzard · 2025-01-07T07:57:41Z

FWIW I find the commit message incomprehensible. What is the difference between doing something, and doing something to completion?

mathlib-bors · 2025-01-07T08:12:53Z

Pull request successfully merged into master.

Build succeeded:

kmill · 2025-01-07T09:59:25Z

@kbuzzard Informally when we say "elaborate a term" it means "start elaborating a term". The resulting expression might have metavariables for postponed problems (typeclasses, coercions, tactic scripts, or postponed elaborators). Maybe "fully elaborate" would be better than "elaborate to completion" — this was supposed to mean "force all postponed problems to complete (or fail with an error message if it's impossible)". The (e :) syntax does not allow e to wait for more information. It's like you did def tmp := e.

* origin/master: (642 commits) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) feat(Analysis/Analytic): lemmas about `smul` for power series (#19816) chore: don't import algebra in `Data.Multiset.Basic` (#19775) ...

* origin/master: (80 commits) chore(CategoryTheory): remove data produced by tactic block (#20565) feat: `|∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ` (#20540) feat: the Boolean subalgebra generated by the lattice generated by a set (#20440) feat: misc. lemmas about moments, tilted measures (#20150) chore(Algebra/Lie): make IsNilpotent and IsSolvable independent of scalars (#20556) feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` (#19373) feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe` (#19377) chore: scope 'on' notation to Function (#20562) chore: disable docPrime linter (#20559) chore: deprecate MulRingNorm._ in favour of AbsoluteValue._ (#20557) fix(scripts/bench_summary): input jobID as a Nat, rather than a String (#20539) chore: move results about `DivisionMonoid` + `HasDistribNeg` (#20551) feat(NumberTheory/NumberField/Embeddings): definition of totally real field (#20542) chore(Noetherian/Artinian): generalize to Semiring (#20534) chore: protect `Filter.nhds_{iInf,inf}` (#20530) chore(AlgebraicTopology): move SplitSimplicialObject.lean (#20511) chore: extract 3 new files out of MeasureSpace (#20509) feat(RingTheory): Jacobian criterion for smoothness of local algebras (#20326) doc(RingTheory/Flat): add reference to Lambek's paper (#20266) feat(NumberTheory/AbelSummation): add more results (#19942) chore(Multilinear/Basic): generalize the `SMul` instance (#20536) feat(FDeriv/Equiv): generalize `HasFDerivAt.of_local_left_inverse` (#20516) feat(ContDiff): add `iteratedFDeriv_comp` (#20472) feat(LowerUpperTopology): add lemmas (#20465) feat(ContDiff): weaken some assumptions (#20368) fix(scripts/technical-debt-metric): avoid division by 0 (#20537) chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528) feat(FTaylorSeries): add lemmas about `dist` between 0th and 1st derivs (#20089) feat: results on inner regularity of finite measures (#19780) chore: to_additive various results on groups, group actions (#20547) feat(Probability/Kernel): `Kernel.sectL` and `sectR` (#15466) chore(CategoryTheory/Limits/Fubini): relax universes constraints and weaken hypotheses (#20553) perf: remove `@[simp]` on `Fintype.card_of{IsEmpty,Subsingleton}` (#20524) fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) chore(Ideal/Basic): dependent generalization of `Ideal.pi` (#20535) feat(RingTheory): being unramified is a local property (#20323) chore(BooleanSubalgebra): use `IsSublattice` in `closure_sdiff_sup_induction` (#20439) feat(Order/SuccPred/CompleteLinearOrder): `⨆ a < x, succ a = x` (#19970) chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) feat(CategoryTheory/Triangulated/Adjunction): the right adjoint of a triangulated functor is triangulated (#20255) chore(Order/SuccPred/LinearLocallyFinite): change data-creating instances to defs (#20235) chore: don't import algebra in `Data.Finset.Basic` (#19779) feat: initial segment commutes with `Iio` (#20503) chore(Measure/Pi): move parts to `MeasurableSpace/` (#20215) chore: smile more often (#20436) chore(Algebra/Category/MonCat/ForgetCorepresentable, Algebra/Group/Equiv/Basic): move definitions and add symmetric version (#20416) feat(GroupTheory/QuotientGroup): group correspondence theorem (#20007) doc: change "module homomorphism" to "linear map" (#20481) perf: improves the performance of the `Repr (Equiv.Perm α)` instance (1/4) (#20519) fix: do not keep only the first line of hints (#19756) ...

chore: smile more often

dbcfee8

eric-wieser force-pushed the smiles branch 4 times, most recently from 6427975 to 7b3b6e3 Compare January 4, 2025 00:33

eric-wieser added 2 commits January 4, 2025 00:34

Fix bad regex replacement

3b27d56

`(e : _)` means something unrelated in binders.

In some cases (e :) doesn't elaborate but (e : _) does

3b93321

eric-wieser force-pushed the smiles branch from 7b3b6e3 to 3b93321 Compare January 4, 2025 00:35

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 4, 2025

Merge remote-tracking branch 'origin/master' into smiles

a75a5a8

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 7, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 7, 2025

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 7, 2025

mathlib-bors bot changed the title ~~chore: smile more often~~ [Merged by Bors] - chore: smile more often Jan 7, 2025

mathlib-bors bot closed this Jan 7, 2025

mathlib-bors bot deleted the smiles branch January 7, 2025 08:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: smile more often#20436

[Merged by Bors] - chore: smile more often#20436
eric-wieser wants to merge 4 commits intomasterfrom
smiles

eric-wieser commented Jan 3, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jan 3, 2025 •

edited

Loading

Declarations diff

Uh oh!

eric-wieser commented Jan 4, 2025

Uh oh!

leanprover-bot commented Jan 4, 2025

Uh oh!

eric-wieser commented Jan 7, 2025

Uh oh!

kmill commented Jan 7, 2025

Uh oh!

eric-wieser commented Jan 7, 2025

Uh oh!

adomani commented Jan 7, 2025

Uh oh!

adomani commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

kbuzzard commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

kmill commented Jan 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

eric-wieser commented Jan 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a75a5a8a48

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser commented Jan 4, 2025

Uh oh!

leanprover-bot commented Jan 4, 2025

Uh oh!

eric-wieser commented Jan 7, 2025

Uh oh!

kmill commented Jan 7, 2025

Uh oh!

eric-wieser commented Jan 7, 2025

Uh oh!

adomani commented Jan 7, 2025

Uh oh!

adomani commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

kbuzzard commented Jan 7, 2025

Uh oh!

mathlib-bors bot commented Jan 7, 2025

Uh oh!

kmill commented Jan 7, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

eric-wieser commented Jan 3, 2025 •

edited

Loading

github-actions bot commented Jan 3, 2025 •

edited

Loading