Theoria.Kernel.Reference.Normalize (theoria v0.4.0)

Reference normalization for kernel differential assurance.

Summary

result()

Reference definitional equality by full normalization.

Computes full normal form with the reference normalizer.

whnf(env, term)

Computes weak-head normal form with the reference normalizer.

@type result() :: {:ok, Theoria.Term.t()} | {:error, :out_of_fuel}

@spec defeq?(Theoria.Env.t(), Theoria.Term.t(), Theoria.Term.t()) :: boolean()

Reference definitional equality by full normalization.

@spec normalize(Theoria.Env.t(), Theoria.Term.t()) :: result()

Computes full normal form with the reference normalizer.

@spec whnf(Theoria.Env.t(), Theoria.Term.t()) :: result()

Computes weak-head normal form with the reference normalizer.