Generators for declarations derived from inductive specs.
Summary
Functions
Generates non-dependent and dependent eliminators for a Bool-like inductive.
Returns eliminator generation capabilities for an inductive spec.
Generates non-dependent and dependent eliminators for supported simple inductives.
Generates eliminators or raises Theoria.Error.
Generates indexed eliminators with iota rule metadata.
Generates the dependent eliminator type for an indexed inductive without iota rules.
Generates non-dependent and dependent eliminators for Theoria's List-like shape.
Generates non-dependent and dependent eliminators for a Nat-like inductive.
Returns true when generic eliminator generation supports the spec.
Returns the reason generic eliminator generation does not support the spec.
Functions
@spec bool_eliminators(Theoria.Inductive.Spec.t(), Theoria.Inductive.Shape.t() | nil) :: [ Theoria.Inductive.Recursor.t() ]
Generates non-dependent and dependent eliminators for a Bool-like inductive.
@spec capabilities(Theoria.Inductive.Spec.t()) :: %{ supported?: boolean(), simple?: boolean(), indexed?: boolean(), recursive?: boolean(), shape: Theoria.Inductive.Shape.kind(), reason: atom() | nil }
Returns eliminator generation capabilities for an inductive spec.
@spec eliminators(Theoria.Inductive.Spec.t()) :: {:ok, [Theoria.Inductive.Recursor.t()]} | {:error, Theoria.Error.t()}
Generates non-dependent and dependent eliminators for supported simple inductives.
@spec eliminators!(Theoria.Inductive.Spec.t()) :: [Theoria.Inductive.Recursor.t()]
Generates eliminators or raises Theoria.Error.
@spec indexed_eliminators(Theoria.Inductive.Spec.t()) :: {:ok, [Theoria.Inductive.Recursor.t()]} | {:error, Theoria.Error.t()}
Generates indexed eliminators with iota rule metadata.
@spec indexed_induction_type(Theoria.Inductive.Spec.t()) :: {:ok, Theoria.Term.t()} | {:error, Theoria.Error.t()}
Generates the dependent eliminator type for an indexed inductive without iota rules.
@spec list_eliminators(Theoria.Inductive.Spec.t(), Theoria.Inductive.Shape.t() | nil) :: [ Theoria.Inductive.Recursor.t() ]
Generates non-dependent and dependent eliminators for Theoria's List-like shape.
@spec nat_eliminators(Theoria.Inductive.Spec.t(), Theoria.Inductive.Shape.t() | nil) :: [ Theoria.Inductive.Recursor.t() ]
Generates non-dependent and dependent eliminators for a Nat-like inductive.
@spec supported?(Theoria.Inductive.Spec.t()) :: boolean()
Returns true when generic eliminator generation supports the spec.
@spec unsupported_reason(Theoria.Inductive.Spec.t()) :: atom() | nil
Returns the reason generic eliminator generation does not support the spec.