Theoria.Equation.Matcher.Indexed.Package (theoria v0.4.0)

Copy Markdown View Source

Experimental/internal API for 0.2; subject to change before 0.3. Coherent package for indexed matcher equation metadata.

Summary

Types

t()

Functions

build(info, env)

Builds the indexed matcher equation metadata package and admits the explicit matcher into the returned package environment.

install(package)

Installs realized indexed matcher equation artifacts into the package environment.

plan_lemmas(package)

Returns the metadata-only lemmas planned for the package.

plan_realization(package)

Builds the recursor-informed realization plan for the package.

plan_statements(package)

Returns the checked indexed statement metadata for the package.

realize(package)

Kernel-checks all generated indexed matcher equation artifacts.

validate(package)

Validates the indexed matcher equation package without realizing theorem proofs.

Types

t()

@type t() :: %Theoria.Equation.Matcher.Indexed.Package{
  env: Theoria.Env.t(),
  equations: [Theoria.Equation.Matcher.Equation.t()],
  info: Theoria.Equation.Info.t(),
  lemmas: [Theoria.Equation.Lemma.t()],
  matcher: Theoria.Env.Matcher.t(),
  spec: Theoria.Equation.Matcher.Spec.t(),
  statements: [Theoria.Equation.Matcher.Equation.t()]
}

Functions

build(info, env)

@spec build(Theoria.Equation.Info.t(), Theoria.Env.t()) ::
  {:ok, t()} | {:error, term()}

Builds the indexed matcher equation metadata package and admits the explicit matcher into the returned package environment.

install(package)

@spec install(t()) :: {:ok, Theoria.Env.t(), [Theoria.Theorem.t()]} | {:error, term()}

Installs realized indexed matcher equation artifacts into the package environment.

plan_lemmas(package)

@spec plan_lemmas(t()) :: [Theoria.Equation.Lemma.t()]

Returns the metadata-only lemmas planned for the package.

plan_realization(package)

@spec plan_realization(t()) ::
  {:ok, Theoria.Equation.Matcher.Indexed.Realization.Plan.t()}

Builds the recursor-informed realization plan for the package.

plan_statements(package)

@spec plan_statements(t()) :: [Theoria.Equation.Matcher.Equation.t()]

Returns the checked indexed statement metadata for the package.

realize(package)

@spec realize(t()) :: {:ok, [Theoria.Equation.Realized.t()]} | {:error, term()}

Kernel-checks all generated indexed matcher equation artifacts.

validate(package)

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

Validates the indexed matcher equation package without realizing theorem proofs.