+ descTruncGT
+ descTruncGT_aux
+ instance (X : C) (a b : ℤ) :
+ instance (X : C) (a b : ℤ) : t.IsGE ((t.truncGELE a b).obj X) a := by
+ instance (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGT b).obj X) a := by
+ instance (X : C) (a b : ℤ) [t.IsLE X b] :
+ instance (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncLE a).obj X) b := by
+ instance (X : C) (n : ℤ) : IsIso ((t.truncLE n).map ((t.truncLEι n).app X))
+ instance (X : C) (n : ℤ) [t.IsLE X n] : IsIso ((t.truncLEι n).app X) := by
+ instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT (n - 1)).obj X) n
+ instance (n : ℤ) (X : C) : t.IsGE ((t.truncGT n).obj X) (n + 1)
+ instance (n : ℤ) (X : C) : t.IsLE ((t.truncLE n).obj X) n
+ instance (n : ℤ) : (t.truncGT n).Additive := by
+ instance (n : ℤ) : (t.truncLE n).Additive := by
+ isGE_iff_isIso_truncGTπ_app
+ isGE_iff_isZero_truncLE_obj
+ isGE_truncGT_obj
+ isIso_truncGT_map_iff
+ isIso_truncGT_map_truncGTπ_app
+ isIso_truncLE_map_iff
+ isIso_truncLE_map_truncLEι_app
+ isIso₁_truncLE_map_of_isGE
+ isIso₂_truncGT_map_of_isLE
+ isLE_iff_isIso_truncLEι_app
+ isLE_iff_isZero_truncGT_obj
+ isLE_truncLE_obj
+ isZero_truncLE_obj_of_isGE
+ liftTruncLE
+ liftTruncLE_aux
+ liftTruncLE_ι
+ natTransTruncLEOfLE
+ natTransTruncLEOfLE_refl
+ natTransTruncLEOfLE_refl_app
+ natTransTruncLEOfLE_trans
+ natTransTruncLEOfLE_trans_app
+ natTransTruncLEOfLE_ι
+ natTransTruncLEOfLE_ι_app
+ to_truncLE_obj_ext
+ triangleLEGE
+ triangleLEGEIsoTriangleLTGE
+ triangleLEGE_distinguished
+ triangleLEGT
+ triangleLEGTIsoTriangleLEGE
+ triangleLEGT_distinguished
+ truncGELE
+ truncGELEIsoLEGE
+ truncGELEIsoTruncGELT
+ truncGEδLE
+ truncGT
+ truncGTIsoTruncGE
+ truncGTδLE
+ truncGTπ
+ truncLE
+ truncLEGE
+ truncLEIsoTruncLT
+ truncLEIsoTruncLT_hom_ι
+ truncLEIsoTruncLT_hom_ι_app
+ truncLEIsoTruncLT_inv_ι
+ truncLEIsoTruncLT_inv_ι_app
+ truncLEι
+ π_descTruncGT
+ π_truncGTIsoTruncGE_hom
+ π_truncGTIsoTruncGE_hom_ι_app
+ π_truncGTIsoTruncGE_inv
+ π_truncGTIsoTruncGE_inv_ι_app
++ instance (X : C) (a b : ℤ) [t.IsGE X a] :

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

Current commit 19a9188b97
Reference commit 32af1e5dd5

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