Commit 2025-08-16 07:25 3ccdf0c3

chore: use delta deriving for #380 (#28498) The new delta deriving handler from https://github.com/leanprover/lean4/pull/9800 makes it possible to address most of issue #380. There are still some cases that are not handled:

• Some definitions are abbreviations, so there is no point in deriving instances, since they already inherit instances. Plus, adding instances to abbreviations adds intances to the unfolded abbreviation, which might not be wanted.
• Deriving Functor.Full and Functor.Faithful often gives the wrong instance. For example, with Skeleton and fromSkeleton, the derived instances are in terms of InducedCategory, not Skeleton. It might not ever be possible to derive instances in this situation.