+ FullSubcategory.hasForget
+ HasForget
+ HasForget.hasCoeToSort
+ HasForget.instFunLike
+ HasForget.types
+ InducedCategory.hasForget
+ exact_iff_of_hasForget
+ groupWithZeroHasForget
+ hasForgetFintype
+ hasForgetOfDifferentialObjects
+ instance (x : SimplexCategory) : Fintype (HasForget.forget.obj x)
+ instance : HasCoeToSort X := HasForget.hasCoeToSort X
+ instance : HasForget (ContAction V G)
+ instance : HasForget (DiscreteContAction V G)
+ instance : HasForget (FDRep k G) := inferInstance
+ instance : HasForget (FGModuleCat R) := by
+ instance : HasForget (GradedObject β C) where forget := total β C ⋙ forget C
+ instance : HasForget BddDistLat
+ instance : HasForget BddLat
+ instance : HasForget BoolAlg
+ instance : HasForget BoolRing
+ instance : HasForget Born
+ instance : HasForget Compactum where forget := forget
+ instance : HasForget CompleteLat := by
+ instance : HasForget DistLat
+ instance : HasForget FinTopCat
+ instance : HasForget FiniteGrp := InducedCategory.hasForget FiniteGrp.toGrp
+ instance : HasForget Frm := by
+ instance : HasForget HeytAlg := by
+ instance : HasForget Lat
+ instance : HasForget LinOrd
+ instance : HasForget MeasCat := by
+ instance : HasForget NonemptyFinLinOrd
+ instance : HasForget PartOrd
+ instance : HasForget Preord
+ instance : HasForget ProfiniteGrp
+ instance : HasForget SemiNormedGrp := by
+ instance : HasForget SemilatInfCat
+ instance : HasForget SemilatSupCat
+ instance : HasForget TopCommRingCat.{u}
+ instance : HasForget UniformSpaceCat
+ instance : HasForget ωCPO := by unfold ωCPO; infer_instance
+ instance : HasForget.{0} SimplexCategory
+ instance : HasForget.{u} CommRingCat
+ instance : HasForget.{u} CommSemiRingCat
+ instance : HasForget.{u} DeltaGenerated.{u}
+ instance : HasForget.{u} RingCat
+ instance : HasForget.{u} SemiNormedGrp₁
+ instance : HasForget.{u} SemiRingCat
+ instance : HasForget.{u} Sequential.{u}
+ instance : HasForget.{v} (AlgebraCat.{v} R)
+ instance : HasForget.{w} CompactlyGenerated.{u, w}
+ instance [HasForget C] [PreservesColimitsOfShape (Discrete WalkingPair) (forget C)]
+ instance [HasForget V] : HasForget (Action V G)
+ instance {D : Type w} [Category.{w'} D] [HasForget.{max u v} D]
+ moduleHasForget
+++ instHasForget
++++++++++++++++++++ hasForget
- ConcreteCategory.hasCoeToSort
- ConcreteCategory.instFunLike
- ConcreteCategory.types
- FullSubcategory.concreteCategory
- InducedCategory.concreteCategory
- concreteCategoryFintype
- concreteCategoryOfDifferentialObjects
- exact_iff_of_concreteCategory
- groupWithZeroConcreteCategory
- instance (x : SimplexCategory) : Fintype (ConcreteCategory.forget.obj x)
- instance : ConcreteCategory (ContAction V G)
- instance : ConcreteCategory (DiscreteContAction V G)
- instance : ConcreteCategory (FDRep k G) := inferInstance
- instance : ConcreteCategory (FGModuleCat R) := by
- instance : ConcreteCategory (GradedObject β C) where forget := total β C ⋙ forget C
- instance : ConcreteCategory BddDistLat
- instance : ConcreteCategory BddLat
- instance : ConcreteCategory BoolAlg
- instance : ConcreteCategory BoolRing
- instance : ConcreteCategory Born
- instance : ConcreteCategory Compactum where forget := forget
- instance : ConcreteCategory CompleteLat := by
- instance : ConcreteCategory DistLat
- instance : ConcreteCategory FinTopCat
- instance : ConcreteCategory FiniteGrp := InducedCategory.concreteCategory FiniteGrp.toGrp
- instance : ConcreteCategory Frm := by
- instance : ConcreteCategory HeytAlg := by
- instance : ConcreteCategory Lat
- instance : ConcreteCategory LinOrd
- instance : ConcreteCategory MeasCat := by
- instance : ConcreteCategory NonemptyFinLinOrd
- instance : ConcreteCategory PartOrd
- instance : ConcreteCategory Preord
- instance : ConcreteCategory ProfiniteGrp
- instance : ConcreteCategory SemiNormedGrp := by
- instance : ConcreteCategory SemilatInfCat
- instance : ConcreteCategory SemilatSupCat
- instance : ConcreteCategory TopCommRingCat.{u}
- instance : ConcreteCategory UniformSpaceCat
- instance : ConcreteCategory ωCPO := by unfold ωCPO; infer_instance
- instance : ConcreteCategory.{0} SimplexCategory
- instance : ConcreteCategory.{u} CommRingCat
- instance : ConcreteCategory.{u} CommSemiRingCat
- instance : ConcreteCategory.{u} DeltaGenerated.{u}
- instance : ConcreteCategory.{u} RingCat
- instance : ConcreteCategory.{u} SemiNormedGrp₁
- instance : ConcreteCategory.{u} SemiRingCat
- instance : ConcreteCategory.{u} Sequential.{u}
- instance : ConcreteCategory.{v} (AlgebraCat.{v} R)
- instance : ConcreteCategory.{w} CompactlyGenerated.{u, w}
- instance : HasCoeToSort X := ConcreteCategory.hasCoeToSort X
- instance [ConcreteCategory C] [PreservesColimitsOfShape (Discrete WalkingPair) (forget C)]
- instance [ConcreteCategory V] : ConcreteCategory (Action V G)
- instance {D : Type w} [Category.{w'} D] [ConcreteCategory.{max u v} D]
- moduleConcreteCategory
--- instConcreteCategory
-------------------- concreteCategory

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

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