[Merged by Bors] - feat: add `fast_instance%` elaborator by eric-wieser · Pull Request #11521 · leanprover-community/mathlib4

eric-wieser · 2024-03-20T00:05:11Z

Quoting the docstring:

fast_instance% inst takes an expression for a typeclass instance inst, and unfolds it into
constructor applications that leverage existing instances.
For instance, when used as

instance instSemiring : Semiring X := sorry
instance instRing : Ring X := fast_instance% Function.Injective.ring ..

this will define instRing as a nested constructor application that refers to instSemiring.
The advantage is then that instRing.toSemiring unifies almost immediately with instSemiring,
rather than having to break it down into smaller pieces.

Related to #7432

Mathlib.lean

Mathlib/Tactic.lean

Mathlib/Tactic/FastInstance.lean

eric-wieser · 2024-03-20T01:22:35Z

!bench

leanprover-bot · 2024-03-20T02:11:51Z

Here are the benchmark results for commit 02e5f99.
The entire run failed.
Found no significant differences.

eric-wieser · 2024-03-20T08:45:49Z

!bench

leanprover-bot · 2024-03-20T09:10:46Z

Here are the benchmark results for commit f31997b.
The entire run failed.
Found no significant differences.

mattrobball · 2024-03-20T09:36:13Z

Ping me when ready. I think metaprogramming to hide preferred parent and even intermediate structure internals is the future and am glad this got started.

eric-wieser · 2024-03-20T10:31:57Z

Feel free to push things to this branch to get linting passing, so that we have a benchmark.

eric-wieser · 2024-03-20T11:31:10Z

!bench

leanprover-bot · 2024-03-20T11:56:26Z

Here are the benchmark results for commit ce19211.
There were no significant changes against commit 69fd837.

eric-wieser · 2024-03-22T21:51:03Z

!bench

mattrobball · 2024-03-22T21:53:58Z

One comment: I think compact_instance% would be a more fitting name

eric-wieser · 2024-03-22T22:23:00Z

!bench

eric-wieser · 2024-03-22T22:33:41Z

One comment: I think compact_instance% would be a more fitting name

Sure, that sounds reasonable; though I'll refrain from doing so until I have a benchmark that indicates this actually helps.

leanprover-bot · 2024-03-22T22:35:48Z

Here are the benchmark results for commit 3e91dd1.
There were significant changes against commit 69fd837:

  Benchmark                                              Metric         Change
  ============================================================================
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction         instructions   -11.0%
+ ~Mathlib.AlgebraicGeometry.Spec                        instructions   -13.0%
+ ~Mathlib.FieldTheory.AbelRuffini                       instructions   -10.3%
+ ~Mathlib.FieldTheory.Adjoin                            instructions    -8.9%
+ ~Mathlib.FieldTheory.PurelyInseparable                 instructions   -13.0%
+ ~Mathlib.FieldTheory.SeparableDegree                   instructions   -20.0%
+ ~Mathlib.FieldTheory.Subfield                          instructions   -14.6%
+ ~Mathlib.FieldTheory.Subfield.Order                    instructions   -76.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding   instructions    -7.6%
+ ~Mathlib.NumberTheory.NumberField.ClassNumber          instructions   -17.6%
+ ~Mathlib.NumberTheory.NumberField.Discriminant         instructions    -8.5%
+ ~Mathlib.NumberTheory.NumberField.FractionalIdeal      instructions   -20.4%
+ ~Mathlib.NumberTheory.NumberField.Units                instructions    -6.1%
+ ~Mathlib.RingTheory.Subring.Order                      instructions   -79.3%
+ ~Mathlib.RingTheory.Subsemiring.Order                  instructions   -64.4%

mattrobball · 2024-03-22T22:40:36Z

That is pretty good

mattrobball · 2024-03-22T22:45:52Z

I think the changes in #11029 should be useful to focus the use of the compactor. There I just make versions of Function.Injective/Surjective instances taking bundled class instance from the target/source instead of just the data.

eric-wieser · 2024-03-22T22:52:47Z

Huh, I guess the benchmark doesn't care about shake output; so we're going to get a repeat.

What this doesn't tell us is which fast_instance%s are carrying the weight; but maybe we don't care.

eric-wieser · 2024-03-22T22:53:12Z

Mathlib/Algebra/Order/Nonneg/Ring.lean


 instance strictOrderedSemiring [StrictOrderedSemiring α] :
    StrictOrderedSemiring { x : α // 0 ≤ x } :=
+  -- fast_instance% -- TODO: fix


There's something weird happening with a free variable on this one.

leanprover-bot · 2024-03-22T22:59:53Z

Here are the benchmark results for commit 27f7d47.
There were significant changes against commit 69fd837:

  Benchmark                                              Metric         Change
  ============================================================================
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction         instructions   -11.0%
+ ~Mathlib.AlgebraicGeometry.Spec                        instructions   -13.0%
+ ~Mathlib.FieldTheory.AbelRuffini                       instructions   -10.3%
+ ~Mathlib.FieldTheory.Adjoin                            instructions    -8.9%
+ ~Mathlib.FieldTheory.PurelyInseparable                 instructions   -13.0%
+ ~Mathlib.FieldTheory.SeparableDegree                   instructions   -20.0%
+ ~Mathlib.FieldTheory.Subfield                          instructions   -14.6%
+ ~Mathlib.FieldTheory.Subfield.Order                    instructions   -76.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding   instructions    -7.6%
+ ~Mathlib.NumberTheory.NumberField.ClassNumber          instructions   -17.6%
+ ~Mathlib.NumberTheory.NumberField.Discriminant         instructions    -8.5%
+ ~Mathlib.NumberTheory.NumberField.FractionalIdeal      instructions   -20.4%
+ ~Mathlib.NumberTheory.NumberField.Units                instructions    -6.1%
+ ~Mathlib.RingTheory.Subring.Order                      instructions   -79.3%
+ ~Mathlib.RingTheory.Subsemiring.Order                  instructions   -64.4%

eric-wieser · 2024-03-22T23:35:33Z

!bench

mattrobball · 2024-03-22T23:46:14Z

RingTheory.NonUnitalSubsemiring.Basic is another target.

leanprover-bot · 2024-03-23T00:00:50Z

Here are the benchmark results for commit d633325.
There were significant changes against commit 69fd837:

  Benchmark                                              Metric         Change
  ============================================================================
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction         instructions   -11.0%
+ ~Mathlib.AlgebraicGeometry.Spec                        instructions   -13.0%
+ ~Mathlib.FieldTheory.AbelRuffini                       instructions   -45.4%
+ ~Mathlib.FieldTheory.Adjoin                            instructions    -9.9%
+ ~Mathlib.FieldTheory.PurelyInseparable                 instructions   -13.1%
+ ~Mathlib.FieldTheory.SeparableDegree                   instructions   -20.4%
+ ~Mathlib.FieldTheory.Subfield                          instructions   -14.6%
+ ~Mathlib.FieldTheory.Subfield.Order                    instructions   -76.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding   instructions    -7.7%
+ ~Mathlib.NumberTheory.NumberField.ClassNumber          instructions   -17.6%
+ ~Mathlib.NumberTheory.NumberField.Discriminant         instructions    -8.5%
+ ~Mathlib.NumberTheory.NumberField.FractionalIdeal      instructions   -20.4%
+ ~Mathlib.NumberTheory.NumberField.Units                instructions    -6.1%
+ ~Mathlib.NumberTheory.RamificationInertia              instructions    -3.9%
+ ~Mathlib.RingTheory.Subring.Order                      instructions   -79.3%
+ ~Mathlib.RingTheory.Subsemiring.Order                  instructions   -64.4%

github-actions · 2025-01-17T19:17:26Z

PR summary 37b82b8ef1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.FastInstance` (new file)	2

Declarations diff

+ CommMagma
+ CommSemigroup
+ Dec
+ Function.Injective.commMagma
+ Function.Injective.commSemigroup
+ Function.Injective.semigroup
+ Mul
+ Semigroup
+ Wrapped.instField
+ dec1
+ dec2
+ elabFastInstance
+ fastInstance
+ instCommSemigroup
+ instRing
+ instSemigroup
+ instSemiring
+ instance : Add (Wrapped α) where add := fun ⟨m⟩ ⟨n⟩ => ⟨m + n⟩
+ instance : Div (Wrapped α) where div m n := ⟨Div.div m.1 n.1⟩
+ instance : Inf (Wrapped α) where inf s t := ⟨Inf.inf s.1 t.1⟩
+ instance : IntCast (Wrapped α) where intCast n := ⟨IntCast.intCast n⟩
+ instance : Inv (Wrapped α) where inv m := ⟨Inv.inv m.1⟩
+ instance : Mul (Wrapped α) where mul := fun ⟨m⟩ ⟨n⟩ => ⟨m * n⟩
+ instance : Mul Nat := ⟨(· * · )⟩
+ instance : NNRatCast (Wrapped α) where nnratCast n := ⟨NNRatCast.nnratCast n⟩
+ instance : NatCast (Wrapped α) where natCast n := ⟨NatCast.natCast n⟩
+ instance : Neg (Wrapped α) where neg m := ⟨Neg.neg m.1⟩
+ instance : One (Wrapped α) where one := ⟨1⟩
+ instance : Pow (Wrapped α) ℕ where pow m n := ⟨Pow.pow m.1 n⟩
+ instance : Pow (Wrapped α) ℤ where pow m n := ⟨Pow.pow m.1 n⟩
+ instance : RatCast (Wrapped α) where ratCast n := ⟨RatCast.ratCast n⟩
+ instance : SMul ℕ (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : SMul ℚ (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : SMul ℚ≥0 (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : SMul ℤ (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : Sub (Wrapped α) where sub m n := ⟨Sub.sub m.1 n.1⟩
+ instance : Sup (Wrapped α) where sup s t := ⟨Sup.sup s.1 t.1⟩
+ instance : Zero (Wrapped α) where zero := ⟨0⟩
+ instance [Mul α] : Mul (Wrapped α) where mul m n := ⟨Mul.mul m.1 n.1⟩
+ slowInstance
++ Wrapped
++ val_injective

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).

Mathlib/Tactic/FastInstance.lean

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

github-actions · 2025-01-22T21:14:38Z

PR summary d0a3b12d12

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.FastInstance` (new file)	20

Declarations diff

+ CommMagma
+ CommSemigroup
+ Dec
+ Function.Injective.commMagma
+ Function.Injective.commSemigroup
+ Function.Injective.semigroup
+ Mul
+ Semigroup
+ Wrapped.instField
+ dec1
+ dec2
+ elabFastInstance
+ fastInstance
+ instCommSemigroup
+ instRing
+ instSemigroup
+ instSemiring
+ instance : Add (Wrapped α) where add := fun ⟨m⟩ ⟨n⟩ => ⟨m + n⟩
+ instance : Div (Wrapped α) where div m n := ⟨Div.div m.1 n.1⟩
+ instance : Inf (Wrapped α) where inf s t := ⟨Inf.inf s.1 t.1⟩
+ instance : IntCast (Wrapped α) where intCast n := ⟨IntCast.intCast n⟩
+ instance : Inv (Wrapped α) where inv m := ⟨Inv.inv m.1⟩
+ instance : Mul (Wrapped α) where mul := fun ⟨m⟩ ⟨n⟩ => ⟨m * n⟩
+ instance : Mul Nat := ⟨(· * · )⟩
+ instance : NNRatCast (Wrapped α) where nnratCast n := ⟨NNRatCast.nnratCast n⟩
+ instance : NatCast (Wrapped α) where natCast n := ⟨NatCast.natCast n⟩
+ instance : Neg (Wrapped α) where neg m := ⟨Neg.neg m.1⟩
+ instance : One (Wrapped α) where one := ⟨1⟩
+ instance : Pow (Wrapped α) ℕ where pow m n := ⟨Pow.pow m.1 n⟩
+ instance : Pow (Wrapped α) ℤ where pow m n := ⟨Pow.pow m.1 n⟩
+ instance : RatCast (Wrapped α) where ratCast n := ⟨RatCast.ratCast n⟩
+ instance : SMul ℕ (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : SMul ℚ (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : SMul ℚ≥0 (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : SMul ℤ (Wrapped α) where smul n m := ⟨SMul.smul n m.1⟩
+ instance : Sub (Wrapped α) where sub m n := ⟨Sub.sub m.1 n.1⟩
+ instance : Sup (Wrapped α) where sup s t := ⟨Sup.sup s.1 t.1⟩
+ instance : Zero (Wrapped α) where zero := ⟨0⟩
+ instance [Mul α] : Mul (Wrapped α) where mul m n := ⟨Mul.mul m.1 n.1⟩
+ slowInstance
++ Wrapped
++ val_injective

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).

github-actions · 2025-01-22T21:17:59Z

PR summary 8e6f7431b6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.FastInstance` (new file)	20

Declarations diff

+ CommMagma
+ CommSemigroup
+ Dec
+ Function.Injective.commMagma
+ Function.Injective.commSemigroup
+ Function.Injective.semigroup
+ Mul
+ Semigroup
+ Wrapped
+ dec1
+ dec2
+ elabFastInstance
+ instCommSemigroup
+ instRing
+ instSemigroup
+ instSemiring
+ instance : Mul Nat := ⟨(· * · )⟩
+ instance [Mul α] : Mul (Wrapped α) where mul m n := ⟨Mul.mul m.1 n.1⟩
+ val_injective

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).

Mathlib/Tactic/FastInstance.lean

mattrobball · 2025-01-22T21:28:31Z

!bench

adomani · 2025-01-22T21:29:22Z

Should there also be a test with a measure of some heartbeat count that is smaller with fast_instance% than without?

Co-authored-by: damiano <adomani@gmail.com>

github-actions · 2025-01-22T21:31:50Z

PR summary 92e327721c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.FastInstance` (new file)	20

Declarations diff

+ CommMagma
+ CommSemigroup
+ Dec
+ Function.Injective.commMagma
+ Function.Injective.commSemigroup
+ Function.Injective.semigroup
+ Mul
+ Semigroup
+ Wrapped
+ dec1
+ dec2
+ elabFastInstance
+ instCommSemigroup
+ instRing
+ instSemigroup
+ instSemiring
+ instance : Mul Nat := ⟨(· * · )⟩
+ instance [Mul α] : Mul (Wrapped α) where mul m n := ⟨Mul.mul m.1 n.1⟩
+ val_injective

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).

leanprover-bot · 2025-01-22T21:57:40Z

Here are the benchmark results for commit 8e6f743.
There were no significant changes against commit 80283e8.

github-actions · 2025-01-22T21:58:09Z

File	Instructions	%
`build`	+20.981⬝10⁹	(+0.01%)
CI run

mattrobball · 2025-01-22T21:59:16Z

Of course, I forgot that the applications are split off now.

adomani · 2025-01-22T22:07:44Z

I wonder why the PR summary now posts a new comment, rather than updating the old ones. It seems to be limited to this PR, though.

github-actions · 2025-01-23T16:33:08Z

PR summary 55bc9b1daa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.FastInstance` (new file)	20

Declarations diff

+ CommMagma
+ CommSemigroup
+ Dec
+ Function.Injective.commMagma
+ Function.Injective.commSemigroup
+ Function.Injective.semigroup
+ Mul
+ Semigroup
+ Wrapped
+ dec1
+ dec2
+ elabFastInstance
+ instCommSemigroup
+ instRing
+ instSemigroup
+ instSemiring
+ instance : Mul Nat := ⟨(· * · )⟩
+ instance [Mul α] : Mul (Wrapped α) where mul m n := ⟨Mul.mul m.1 n.1⟩
+ val_injective

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).

mattrobball · 2025-01-23T16:34:49Z

#20993 has the original changes mostly working on a current master. ~~We has some shenanigans with unknown free variables etc. now though~~ Not on current master

github-actions · 2025-01-23T16:56:18Z

PR summary 56ec6a243b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	1
`Mathlib.Tactic.FastInstance` (new file)	20

Declarations diff

+ CommMagma
+ CommSemigroup
+ Dec
+ Function.Injective.commMagma
+ Function.Injective.commSemigroup
+ Function.Injective.semigroup
+ Mul
+ Semigroup
+ Wrapped
+ dec1
+ dec2
+ elabFastInstance
+ instCommSemigroup
+ instRing
+ instSemigroup
+ instSemiring
+ instance : Mul Nat := ⟨(· * · )⟩
+ instance [Mul α] : Mul (Wrapped α) where mul m n := ⟨Mul.mul m.1 n.1⟩
+ val_injective

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).

mattrobball · 2025-01-23T17:57:39Z

Given the effects of #20933, I will merge this in ~3 hours (after classes) unless anyone objects.

mattrobball · 2025-01-23T21:13:23Z

bors merge

Quoting the docstring: `fast_instance% inst` takes an expression for a typeclass instance `inst`, and unfolds it into constructor applications that leverage existing instances. For instance, when used as ```lean instance instSemiring : Semiring X := sorry instance instRing : Ring X := fast_instance% Function.Injective.ring .. ``` this will define `instRing` as a nested constructor application that refers to `instSemiring`. The advantage is then that `instRing.toSemiring` unifies almost immediately with `instSemiring`, rather than having to break it down into smaller pieces. Related to #7432 Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

mathlib-bors · 2025-01-23T21:22:07Z

Pull request successfully merged into master.

Build succeeded:

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes. t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Mar 20, 2024

github-actions bot reviewed Mar 20, 2024

View reviewed changes

Mathlib.lean Outdated Show resolved Hide resolved

Mathlib.lean Show resolved Hide resolved

Mathlib/Tactic.lean Outdated Show resolved Hide resolved

Mathlib/Tactic.lean Show resolved Hide resolved

github-actions bot reviewed Mar 20, 2024

View reviewed changes

Mathlib/Tactic/FastInstance.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/FastInstance.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/FastInstance.lean Outdated Show resolved Hide resolved

github-actions bot reviewed Mar 20, 2024

View reviewed changes

Mathlib/Tactic/FastInstance.lean Outdated Show resolved Hide resolved

eric-wieser mentioned this pull request Mar 20, 2024

[Merged by Bors] - chore: Rename coe_nat/coe_int/coe_rat to natCast/intCast/ratCast #11499

Closed

3 tasks

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 20, 2024

eric-wieser mentioned this pull request Mar 20, 2024

perf(Sub*): use direct inheritance for algebraic instances on subtypes #10617

Closed

1 task

eric-wieser commented Mar 22, 2024

View reviewed changes

Merge branch 'master' into fast_instance

37b82b8

grunweg reviewed Jan 18, 2025

View reviewed changes

Mathlib/Tactic/FastInstance.lean Show resolved Hide resolved

Update Mathlib/Tactic/FastInstance.lean

d0a3b12

Co-authored-by: grunweg <rothgami@math.hu-berlin.de>

remove

8e6f743

adomani reviewed Jan 22, 2025

View reviewed changes

Mathlib/Tactic/FastInstance.lean Outdated Show resolved Hide resolved

Update Mathlib/Tactic/FastInstance.lean

92e3277

Co-authored-by: damiano <adomani@gmail.com>

fix

55bc9b1

fix

56ec6a2

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

mathlib-bors bot changed the title ~~feat: add fast_instance% elaborator~~ [Merged by Bors] - feat: add fast_instance% elaborator Jan 23, 2025

mathlib-bors bot closed this Jan 23, 2025

mathlib-bors bot deleted the fast_instance branch January 23, 2025 21:22

mattrobball mentioned this pull request Jan 27, 2025

[Merged by Bors] - feat(Algebra/Category): ConcreteCategory instances for rings #20815

Closed

1 task

Conversation

eric-wieser commented Mar 20, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser commented Mar 20, 2024

Uh oh!

leanprover-bot commented Mar 20, 2024

Uh oh!

eric-wieser commented Mar 20, 2024

Uh oh!

leanprover-bot commented Mar 20, 2024

Uh oh!

mattrobball commented Mar 20, 2024

Uh oh!

eric-wieser commented Mar 20, 2024

Uh oh!

eric-wieser commented Mar 20, 2024

Uh oh!

leanprover-bot commented Mar 20, 2024

Uh oh!

eric-wieser commented Mar 22, 2024

Uh oh!

mattrobball commented Mar 22, 2024

Uh oh!

eric-wieser commented Mar 22, 2024

Uh oh!

eric-wieser commented Mar 22, 2024

Uh oh!

leanprover-bot commented Mar 22, 2024

Uh oh!

mattrobball commented Mar 22, 2024

Uh oh!

mattrobball commented Mar 22, 2024

Uh oh!

eric-wieser commented Mar 22, 2024

Uh oh!

eric-wieser Mar 22, 2024

Choose a reason for hiding this comment

Uh oh!

leanprover-bot commented Mar 22, 2024

Uh oh!

eric-wieser commented Mar 22, 2024

Uh oh!

mattrobball commented Mar 22, 2024

Uh oh!

leanprover-bot commented Mar 23, 2024

Uh oh!

github-actions bot commented Jan 17, 2025

PR summary 37b82b8ef1

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

github-actions bot commented Jan 22, 2025

PR summary d0a3b12d12

Import changes for modified files

Declarations diff

Uh oh!

github-actions bot commented Jan 22, 2025

PR summary 8e6f7431b6

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

mattrobball commented Jan 22, 2025

Uh oh!

adomani commented Jan 22, 2025

Uh oh!

github-actions bot commented Jan 22, 2025

PR summary 92e327721c

Import changes for modified files

Declarations diff

eric-wieser commented Mar 20, 2024 •

edited

Loading

mattrobball commented Jan 23, 2025 •

edited

Loading