Theoria.Kernel.ConstantAdmission (theoria v0.5.0)

Copy Markdown View Source

Trusted-adjacent admission checks for constants and axioms.

Summary

Functions

add_axiom(env, name, type, universe_params \\ [])
add_constant(env, name, type, universe_params \\ [], opts \\ [])

Functions

add_axiom(env, name, type, universe_params \\ [])

@spec add_axiom(Theoria.Env.t(), Theoria.Env.name(), Theoria.Term.t(), [atom()]) ::
  {:ok, Theoria.Env.t()} | {:error, Theoria.Error.t()}

add_constant(env, name, type, universe_params \\ [], opts \\ [])

@spec add_constant(
  Theoria.Env.t(),
  Theoria.Env.name(),
  Theoria.Term.t(),
  [atom()],
  keyword()
) ::
  {:ok, Theoria.Env.t()} | {:error, Theoria.Error.t()}