Commit 2023-04-18 03:36 7fcd6d8d

feat: Fintype deriving handler (#3198) Adds a handler to derive Fintype instances for non-recursive types without indices. Has an optimized implementation for enum types as well where it produces an underlying list (enumList) of its elements. For non-enum types, the Fintype instance comes from an equivalence to a "proxy type" made from Sum, Sigma, PLift, Empty, and Unit. Also adds a derive_fintype% elaborator to derive Fintype instances in the middle of terms. This is useful in case, for example, a Fintype instance needs an additional DecidableEq instance. This elaborator is defined in terms of a proxy_equiv% elaborator that constructs the proxy type and the the equivalence from it. The machinery for proxy_equiv% is made to be somewhat configurable.