Theoria.Theorem (theoria v0.3.0)

A theorem accepted by the trusted kernel.

Summary

t()

Checks and installs every theorem registered by a theorem module in order.

Adds a checked theorem to an environment as an opaque theorem declaration.

Returns trusted axioms used by a checked theorem.

Checks every theorem registered by a use Theoria.DSL theorem module.

@type t() :: %Theoria.Theorem{
  name: Theoria.Env.name(),
  proof: Theoria.Term.t(),
  type: Theoria.Term.t(),
  universe_params: [atom()]
}

@spec add_all_to_env(module(), Theoria.Env.t()) ::
  {:ok, Theoria.Env.t(), [t()]} | {:error, {atom(), Theoria.Error.t()}}

Checks and installs every theorem registered by a theorem module in order.

@spec add_to_env(Theoria.Env.t(), t()) ::
  {:ok, Theoria.Env.t()} | {:error, Theoria.Error.t()}

Adds a checked theorem to an environment as an opaque theorem declaration.

@spec axioms(Theoria.Env.t(), t()) :: {:ok, MapSet.t(atom())}

Returns trusted axioms used by a checked theorem.

@spec check_all(module(), Theoria.Env.t()) ::
  {:ok, [t()]} | {:error, {atom(), Theoria.Error.t()}}

Checks every theorem registered by a use Theoria.DSL theorem module.