+ instance (priority := 900) (a b : α) : Decidable (a < b) := LinearOrder.decidableLT a b
+ instance (priority := 900) (a b : α) : Decidable (a = b) := LinearOrder.decidableEq a b
+ instance (priority := 900) (a b : α) : Decidable (a ≤ b) := LinearOrder.decidableLE a b
++-- le_iff_lt_or_eq
++-- lt_or_eq_of_le
- instance (priority := 900) (a b : α) : Decidable (a < b)
- instance (priority := 900) (a b : α) : Decidable (a = b)
- instance (priority := 900) (a b : α) : Decidable (a ≤ b)

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