Theoria.Equation.Eqns (theoria v0.3.0)

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

Summary

Functions

database(env, opts \\ [])

Builds a rewrite database from all generated equation metadata in an environment.

generated(env, name)

Returns generated equation lemma metadata for a definition.

get(env, name)

Returns generated equation theorem names for a definition.

install(env, name, opts \\ [])

Installs generated equation theorems for one definition.

install_all(env, opts \\ [])

Installs all generated equation theorems in declaration order.

installed?(env, name)

Returns true when every generated equation theorem for a definition is installed.

realize(env, name)

Realizes generated equation theorem metadata without installing it.

rules(env, name, opts \\ [])

Builds rewrite rules for generated equations of one definition.

source(env, theorem_name)

Finds the source definition for a generated equation theorem name.

unfold(env, name)

Returns generated unfold equation lemma metadata for a definition.

Functions

database(env, opts \\ [])

@spec database(
  Theoria.Env.t(),
  keyword()
) :: Theoria.Rewrite.Database.t()

Builds a rewrite database from all generated equation metadata in an environment.

generated(env, name)

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

Returns generated equation lemma metadata for a definition.

get(env, name)

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

Returns generated equation theorem names for a definition.

install(env, name, opts \\ [])

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

Installs generated equation theorems for one definition.

install_all(env, opts \\ [])

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

Installs all generated equation theorems in declaration order.

installed?(env, name)

@spec installed?(Theoria.Env.t(), atom()) :: boolean()

Returns true when every generated equation theorem for a definition is installed.

realize(env, name)

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

Realizes generated equation theorem metadata without installing it.

rules(env, name, opts \\ [])

@spec rules(Theoria.Env.t(), atom(), keyword()) ::
  {:ok, [Theoria.Rewrite.Rule.t()]} | {:error, term()}

Builds rewrite rules for generated equations of one definition.

source(env, theorem_name)

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

Finds the source definition for a generated equation theorem name.

unfold(env, name)

@spec unfold(Theoria.Env.t(), atom()) ::
  {:ok, Theoria.Equation.Lemma.t()} | {:error, term()}

Returns generated unfold equation lemma metadata for a definition.