Theoria.Kernel.TheoremAdmission (theoria v0.5.0)

Copy Markdown View Source

Trusted-adjacent admission checks for opaque theorem declarations.

Summary

Functions

add(env, name, type, proof, universe_params \\ [])

Functions

add(env, name, type, proof, universe_params \\ [])

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