Theoria.Kernel.Reference (theoria v0.4.0)

Slow, explicit reference checker for the first Theoria kernel fragment.

Summary

result()

Reference type checking for the supported core fragment.

infer(env, term)

Reference type inference for the supported core fragment.

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

@spec check(Theoria.Env.t(), Theoria.Term.t(), Theoria.Term.t()) ::
  :ok | {:error, Theoria.Error.t()}

Reference type checking for the supported core fragment.

@spec check(Theoria.Env.t(), Theoria.Context.t(), Theoria.Term.t(), Theoria.Term.t()) ::
  :ok | {:error, Theoria.Error.t()}

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

Reference type inference for the supported core fragment.

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