FinEnum derivation macro

Provides a FinEnum deriving handler that automatically synthesizes FinEnum instances for inductive types whose constructors are all nullary.

def FinEnum.derive (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Produces a FinEnum instance for the given inductive. It assumes that all constructors are nullary

Equations

• One or more equations did not get rendered due to their size.

def FinEnum.«command#FinEnum.derive_» : Lean.ParserDescr

Standalone instance of FinEnum

Equations

• One or more equations did not get rendered due to their size.