Deriving Handler for Shrinkable

This file defines a handler which automatically derives Shrinkable instances for inductive types.

The derived shrinker for a value C x₁ ... xₙ produces:

1. Subterm shrinks: any xᵢ whose type equals the inductive type itself (these are strictly smaller subterms).
2. Argument shrinks: for each xᵢ, shrink it via its Shrinkable instance and reconstruct the constructor with the shrunk value, holding all other arguments fixed.

Example usage:

inductive Tree where
  | Leaf : Tree
  | Node : Nat → Tree → Tree → Tree
  deriving Shrinkable

To view the derived code, enable the trace class:

set_option trace.plausible.deriving.shrinkable true

Helpers (adapted from Plausible.DeriveArbitrary)

Core shrink-expression builder

Auxiliary function and instance generation