+ instance : AddGroup C_c(α, β) := fast_instance%
+ instance [AddCommGroup β] [IsTopologicalAddGroup β] : AddCommGroup C_c(α, β) := fast_instance%
+ instance [AddCommMonoid β] [ContinuousAdd β] : AddCommMonoid C_c(α, β) := fast_instance%
+ instance [AddMonoid β] [ContinuousAdd β] : AddMonoid C_c(α, β) := fast_instance%
+ instance [AddZeroClass β] [ContinuousAdd β] : AddZeroClass C_c(α, β) := fast_instance%
+ instance [CommMonoid β] [ContinuousMul β] : CommMonoid C(α, β) := fast_instance%
+ instance [CommMonoidWithZero β] [ContinuousMul β] : CommMonoidWithZero C(α, β) := fast_instance%
+ instance [CommSemigroup β] [ContinuousMul β] : CommSemigroup C(α, β) := fast_instance%
+ instance [Group β] [IsTopologicalGroup β] : Group C(α, β) := fast_instance%
+ instance [Monoid β] [ContinuousMul β] : Monoid C(α, β) := fast_instance%
+ instance [MonoidWithZero β] [ContinuousMul β] : MonoidWithZero C(α, β) := fast_instance%
+ instance [MulOneClass β] [ContinuousMul β] : MulOneClass C(α, β) := fast_instance%
+ instance [MulZeroClass β] [ContinuousMul β] : MulZeroClass C(α, β) := fast_instance%
+ instance [MulZeroClass β] [ContinuousMul β] : MulZeroClass C_c(α, β) := fast_instance%
+ instance [NonUnitalRing β] [IsTopologicalRing β] : NonUnitalRing C_c(α, β) := fast_instance%
+ instance [Semigroup β] [ContinuousMul β] : Semigroup C(α, β) := fast_instance%
+ instance [SemigroupWithZero β] [ContinuousMul β] : SemigroupWithZero C(α, β) := fast_instance%
+-+- semilatticeInf
+-+- semilatticeSup
- instance : AddGroup C_c(α, β)
- instance [AddCommGroup β] [IsTopologicalAddGroup β] : AddCommGroup C_c(α, β)
- instance [AddCommMonoid β] [ContinuousAdd β] : AddCommMonoid C_c(α, β)
- instance [AddMonoid β] [ContinuousAdd β] : AddMonoid C_c(α, β)
- instance [AddZeroClass β] [ContinuousAdd β] : AddZeroClass C_c(α, β)
- instance [CommMonoid β] [ContinuousMul β] : CommMonoid C(α, β)
- instance [CommMonoidWithZero β] [ContinuousMul β] : CommMonoidWithZero C(α, β)
- instance [CommSemigroup β] [ContinuousMul β] : CommSemigroup C(α, β)
- instance [Group β] [IsTopologicalGroup β] : Group C(α, β)
- instance [Monoid β] [ContinuousMul β] : Monoid C(α, β)
- instance [MonoidWithZero β] [ContinuousMul β] : MonoidWithZero C(α, β)
- instance [MulOneClass β] [ContinuousMul β] : MulOneClass C(α, β)
- instance [MulZeroClass β] [ContinuousMul β] : MulZeroClass C(α, β)
- instance [MulZeroClass β] [ContinuousMul β] : MulZeroClass C_c(α, β)
- instance [NonUnitalRing β] [IsTopologicalRing β] : NonUnitalRing C_c(α, β)
- instance [Semigroup β] [ContinuousMul β] : Semigroup C(α, β)
- instance [SemigroupWithZero β] [ContinuousMul β] : SemigroupWithZero C(α, β)
-++- partialOrder

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

You can run this locally as

./scripts/reporting/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).