Theoria.Equation.Realized (theoria v0.3.0)

A kernel-checked generated equation artifact that is not necessarily installed as a theorem.

Summary

Types

t()

Functions

check(env, identity, type, proof, opts \\ [])

Builds and kernel-checks a generated equation artifact.

install(env, realized)

Installs a realized equation artifact as an opaque theorem declaration.

to_theorem(realized)

Converts a realized equation artifact to an installable theorem declaration.

Types

t()

@type t() :: %Theoria.Equation.Realized{
  identity: Theoria.Equation.Identity.t(),
  proof: Theoria.Term.t(),
  type: Theoria.Term.t(),
  universe_params: [atom()]
}

Functions

check(env, identity, type, proof, opts \\ [])

@spec check(
  Theoria.Env.t(),
  Theoria.Equation.Identity.t(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  keyword()
) :: {:ok, t()} | {:error, Theoria.Error.t()}

Builds and kernel-checks a generated equation artifact.

install(env, realized)

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

Installs a realized equation artifact as an opaque theorem declaration.

to_theorem(realized)

@spec to_theorem(t()) :: Theoria.Theorem.t()

Converts a realized equation artifact to an installable theorem declaration.