Deriving Handler for Arbitrary

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

(Note that the deriving handler technically derives ArbitraryFueled instancces, but every ArbitraryFueled instance automatically results in an Arbitrary instance, as detailed in Arbitrary.lean.)

Note that the resulting Arbitrary and ArbitraryFueled instance should be considered to be opaque, following the convention for the deriving handler for Mathlib's Encodable typeclass.

Example usage:

-- Datatype for binary trees
inductive Tree
  | Leaf : Tree
  | Node : Nat → Tree → Tree → Tree
  deriving Arbitrary

To sample from a derived generator, users can simply call Arbitrary.runArbitrary, specify the type for the desired generated values and provide some Nat to act as the generator's fuel parameter (10 in the example below):

#eval Arbitrary.runArbitrary (α := Tree) 10

To view the code for the derived generator, users can enable trace messages using the plausible.deriving.arbitrary trace class as follows:

set_option trace.plausible.deriving.arbitrary true

Main definitions

• Deriving handler for ArbitraryFueled typeclass