Theoria.Kernel.Reference (theoria v0.5.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.

Core term constructors not covered by the reference checker.

@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()

@spec unsupported_terms() :: [module()]

Core term constructors not covered by the reference checker.