Theoria.Kernel (theoria v0.1.0)

The trusted type-checking kernel.

The kernel is intentionally small: all DSLs, tactics, and automation must reduce to core terms that are accepted here before a theorem is trusted.

Summary

Types

result()

Functions

add_constant(env, name, type)

add_definition(env, name, type, value)

check(env, term, expected)

check(env, context, lam, expected)

infer(env, term)

infer(env, context, arg3)

Types

result()

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

Functions

add_constant(env, name, type)

add_definition(env, name, type, value)

check(env, term, expected)

check(env, context, lam, expected)

infer(env, term)

infer(env, context, arg3)