Theoria.Equation.Schema (theoria v0.4.0)

Experimental/internal API for 0.2; subject to change before 0.3. Schema metadata for generating equation lemmas from compiled definitions.

Summary

Types

t()

Functions

equation(suffix, left, right, equality_type, opts \\ [])

Builds one schematic equation entry.

new(family, equations, opts \\ [])

Builds equation generation schema metadata.

validate(schema)

Validates equation schema metadata before it drives theorem generation.

Types

t()

@type t() :: %Theoria.Equation.Schema{
  argument_binders: [Theoria.Equation.Schema.Equation.binder()],
  equations: [Theoria.Equation.Schema.Equation.t()],
  family: atom(),
  parameter_binders: [Theoria.Equation.Schema.Equation.binder()],
  recursive_argument: non_neg_integer() | nil
}

Functions

equation(suffix, left, right, equality_type, opts \\ [])

@spec equation(
  atom(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  keyword()
) ::
  Theoria.Equation.Schema.Equation.t()

Builds one schematic equation entry.

new(family, equations, opts \\ [])

@spec new(atom(), [Theoria.Equation.Schema.Equation.t()], keyword()) :: t()

Builds equation generation schema metadata.

validate(schema)

@spec validate(t()) :: :ok | {:error, term()}

Validates equation schema metadata before it drives theorem generation.