Theoria.Kernel.Differential (theoria v0.5.0)

Copy Markdown View Source

Production/reference kernel differential checks.

Summary

Functions

compare_check(env, name, term, type)

Compares production and reference checking for one term/type pair.

compare_defeq(env, name, left, right)

Compares production and reference definitional equality for one pair.

compare_infer(env, name, term)

Compares production and reference inference for one term.

compare_normalize(env, name, term)

Compares production and reference normalization for one term.

compare_theorem(env, theorem)

Compares production and reference checking for a theorem artifact.

run(env)

Runs the default kernel differential corpus.

Functions

compare_check(env, name, term, type)

@spec compare_check(Theoria.Env.t(), atom(), Theoria.Term.t(), Theoria.Term.t()) ::
  :ok | {:error, Theoria.Kernel.Differential.Report.failure()}

Compares production and reference checking for one term/type pair.

compare_defeq(env, name, left, right)

@spec compare_defeq(Theoria.Env.t(), atom(), Theoria.Term.t(), Theoria.Term.t()) ::
  :ok | {:error, Theoria.Kernel.Differential.Report.failure()}

Compares production and reference definitional equality for one pair.

compare_infer(env, name, term)

@spec compare_infer(Theoria.Env.t(), atom(), Theoria.Term.t()) ::
  :ok | {:error, Theoria.Kernel.Differential.Report.failure()}

Compares production and reference inference for one term.

compare_normalize(env, name, term)

@spec compare_normalize(Theoria.Env.t(), atom(), Theoria.Term.t()) ::
  :ok | {:error, Theoria.Kernel.Differential.Report.failure()}

Compares production and reference normalization for one term.

compare_theorem(env, theorem)

@spec compare_theorem(Theoria.Env.t(), Theoria.Theorem.t()) ::
  :ok | {:error, Theoria.Kernel.Differential.Report.failure()}

Compares production and reference checking for a theorem artifact.

run(env)

@spec run(Theoria.Env.t()) :: Theoria.Kernel.Differential.Report.t()

Runs the default kernel differential corpus.