Shared declaration-admission checks used by trusted kernel entrypoints.
Summary
Functions
Ensures a declaration name is not already present in the environment.
Ensures all universe parameters in a term are declared by the enclosing declaration.
Ensures universe parameters are atoms and contain no duplicates.
Functions
@spec ensure_fresh_declaration(Theoria.Env.t(), Theoria.Env.name()) :: :ok | {:error, Theoria.Error.t()}
Ensures a declaration name is not already present in the environment.
@spec ensure_level_params(Theoria.Term.t(), [atom()]) :: :ok | {:error, Theoria.Error.t()}
Ensures all universe parameters in a term are declared by the enclosing declaration.
@spec ensure_universe_params([atom()]) :: :ok | {:error, Theoria.Error.t()}
Ensures universe parameters are atoms and contain no duplicates.