Theoria.Equation.Matcher.Eqns (theoria v0.3.0)

Experimental/internal API for 0.2; subject to change before 0.3. Lookup helpers for generated matcher equation metadata.

Summary

Functions

all(env)

Returns all generated matcher equation metadata in declaration order.

generated(info)

Returns generated matcher equation metadata for a stored equation definition.

generated(env, matcher_name)

Returns generated matcher equation metadata for a matcher declaration.

get(env, matcher_name)

Returns generated matcher equation theorem names for a matcher.

indexed_generated(info, env)

Returns planned indexed matcher equation metadata for an indexed matcher info package.

indexed_lemmas(info, env)

Returns metadata-only lemmas for planned indexed matcher equation statements.

indexed_realize(info, env, selector)

Realizes a planned indexed matcher equation theorem without installing it.

indexed_realize_all(info, env)

Realizes all planned indexed matcher equation theorems without installing them.

indexed_statement(info, env, selector)

Returns a planned indexed matcher equation theorem statement.

indexed_statements(info, env)

Returns all planned indexed matcher equation theorem statements.

lemmas(env)

Converts matcher equations to theorem-like equation lemmas.

realize(env, theorem_name)

Realizes a generated matcher equation artifact without installing it.

source(env, theorem_name)

Finds the matcher that generated a matcher equation theorem.

Functions

all(env)

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

Returns all generated matcher equation metadata in declaration order.

generated(info)

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

Returns generated matcher equation metadata for a stored equation definition.

generated(env, matcher_name)

@spec generated(Theoria.Env.t(), atom()) ::
  {:ok, [Theoria.Equation.Matcher.Equation.t()]} | {:error, term()}

Returns generated matcher equation metadata for a matcher declaration.

get(env, matcher_name)

@spec get(Theoria.Env.t(), atom()) ::
  {:ok, [Theoria.Equation.Identity.t()]} | {:error, term()}

Returns generated matcher equation theorem names for a matcher.

indexed_generated(info, env)

@spec indexed_generated(Theoria.Equation.Info.t(), Theoria.Env.t()) ::
  {:ok, [Theoria.Equation.Matcher.Equation.t()]} | {:error, term()}

Returns planned indexed matcher equation metadata for an indexed matcher info package.

indexed_lemmas(info, env)

@spec indexed_lemmas(Theoria.Equation.Info.t(), Theoria.Env.t()) ::
  {:ok, [Theoria.Equation.Lemma.t()]} | {:error, term()}

Returns metadata-only lemmas for planned indexed matcher equation statements.

indexed_realize(info, env, selector)

@spec indexed_realize(
  Theoria.Equation.Info.t(),
  Theoria.Env.t(),
  Theoria.Equation.Identity.t() | keyword()
) :: {:ok, Theoria.Theorem.t()} | {:error, term()}

Realizes a planned indexed matcher equation theorem without installing it.

indexed_realize_all(info, env)

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

Realizes all planned indexed matcher equation theorems without installing them.

indexed_statement(info, env, selector)

@spec indexed_statement(
  Theoria.Equation.Info.t(),
  Theoria.Env.t(),
  Theoria.Equation.Identity.t() | keyword()
) :: {:ok, Theoria.Term.t()} | {:error, term()}

Returns a planned indexed matcher equation theorem statement.

indexed_statements(info, env)

@spec indexed_statements(Theoria.Equation.Info.t(), Theoria.Env.t()) ::
  {:ok, [Theoria.Equation.Matcher.Equation.t()]} | {:error, term()}

Returns all planned indexed matcher equation theorem statements.

lemmas(env)

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

Converts matcher equations to theorem-like equation lemmas.

realize(env, theorem_name)

@spec realize(Theoria.Env.t(), Theoria.Equation.Identity.t() | atom()) ::
  {:ok, Theoria.Equation.Realized.t()} | {:error, term()}

Realizes a generated matcher equation artifact without installing it.

source(env, theorem_name)

@spec source(Theoria.Env.t(), Theoria.Equation.Identity.t() | atom()) ::
  {:ok, atom()} | :error

Finds the matcher that generated a matcher equation theorem.