Theoria.Equation.Info (theoria v0.4.0)

@type t() :: %Theoria.Equation.Info{
  clauses: [Theoria.Equation.Clause.t()],
  decl_names: [atom()],
  fixed_params: Theoria.Equation.FixedParams.t(),
  level_params: [atom()],
  matcher: Theoria.Equation.Matcher.Info.t() | nil,
  name: atom(),
  rec_arg_pos: non_neg_integer() | nil,
  schema: Theoria.Equation.Schema.t() | nil,
  type: Theoria.Term.t(),
  value: Theoria.Term.t()
}

Functions

all(env)

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

Returns all stored equation metadata in declaration order.

equation?(env, name)

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

Returns whether an environment declaration has stored equation metadata.

fetch(env, name)

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

Fetches stored equation metadata for an environment declaration.

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

@spec fetch_or_build(Theoria.Env.t(), atom(), keyword()) ::
  {:ok, t()} | {:error, term()}

Fetches stored equation metadata or builds it from a valued declaration.

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

@spec from_env(Theoria.Env.t(), atom(), keyword()) :: {:ok, t()} | {:error, term()}

Builds equation metadata from a checked environment definition or theorem.

new(name, type, value, opts \\ [])

@spec new(atom(), Theoria.Term.t(), Theoria.Term.t(), keyword()) :: t()

Builds equation metadata for a compiled definition.

summary(equation)

@spec summary(t()) :: String.t()

Formats a compact metadata summary.