@spec check_declarations(Theoria.Env.t(), Theoria.Inductive.Spec.t()) ::
  validation_result()

@spec check_spec(Theoria.Env.t(), Theoria.Inductive.Spec.t()) :: validation_result()

@spec classify(Theoria.Inductive.Spec.t()) :: Theoria.Inductive.Shape.t()

@spec complete(Theoria.Inductive.Spec.t()) ::
  {:ok, Theoria.Inductive.Spec.t()} | {:error, Theoria.Error.t()}

@spec declarations(Theoria.Inductive.Spec.t()) ::
  {:ok, [Theoria.Inductive.Declaration.t()]} | {:error, Theoria.Error.t()}

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

@spec report(Theoria.Inductive.Spec.t()) ::
  {:ok, Theoria.Inductive.Report.t()} | {:error, Theoria.Error.t()}

@spec shape(Theoria.Inductive.Spec.t()) :: Theoria.Inductive.Shape.kind()

@spec validate(Theoria.Inductive.Spec.t()) :: validation_result()

@spec verify_env(Theoria.Env.t(), Theoria.Inductive.Spec.t()) :: validation_result()