+ BooleanAlgebra.huntingtonAlgebra
+ BooleanAlgebra.robbinsAlgebra
+ HuntingtonAlgebra
+ RobbinsAlgebra
+ ad_compl_add_compl_add
+ add_compl
+ add_compl'
+ add_compl_eq_compl_add_compl_compl
+ add_eq_compl_mul
+ add_eq_iff_compl_add_compl_eq
+ add_eq_left
+ add_eq_one
+ add_mul
+ add_mul'
+ add_mul_mul_compl
+ add_mul_mul_mul_add_compl
+ add_mul_self
+ add_mul_self_left
+ add_one
+ add_one_smul
+ add_self_eq
+ add_smul
+ add_zero
+ compl_compl
+ compl_eq_compl_add_smul_compl_add
+ compl_eq_compl_add_smul_compl_add'
+ compl_eq_compl_iff
+ compl_eq_iff
+ dahn
+ dahn_PNat
+ dahn_add_coe_PNat
+ dahn_add_dahn
+ dahn_of_one_add_of_three
+ dahn_one
+ dahn_succ
+ dahn_zero
+ delta_add_delta
+ delta_compl_add_add
+ delta_compl_right
+ delta_eq_of_left_compl_eq
+ eq_compl_add_compl_add
+ eq_compl_add_compl_smul_add
+ eq_compl_iff
+ eq_of_add_compl_eq
+ eq_of_eq
+ instance : Mul α
+ instance : One α := ⟨default + defaultᶜ⟩
+ instance : Zero α := ⟨1ᶜ⟩
+ instance [Add α] : HSMul ℕ+ α α
+ isHuntington
+ isHuntington_of_add_zero
+ isHuntington_of_compl_compl_eq
+ isHuntington_of_exists_idempotent
+ isHuntington_of_zero_and_one
+ mul_add
+ mul_add_compl
+ mul_add_eq_zero
+ mul_add_self_left
+ mul_assoc
+ mul_comm
+ mul_compl
+ mul_def
+ mul_mul_compl_add
+ mul_one
+ mul_self
+ mul_zero
+ one_compl
+ one_def
+ one_smul
+ smulAux
+ smul_smul
+ winker
+ zero_add
+ zero_compl
+ zero_mul
+ δ
++ booleanAlgebra

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