Theoria.Kernel (theoria v0.4.0)

Copy Markdown View Source

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_axiom(env, name, type, universe_params \\ [])
add_constant(env, name, type, universe_params \\ [], opts \\ [])
add_definition(env, name, type, value, universe_params \\ [], opts \\ [])
add_inductive(env, spec)
add_matcher(env, spec)
add_theorem(env, name, type, proof, universe_params \\ [])
axioms(env, name)
check(env, term, expected)
check(env, context, lam, expected)
dependencies(env, name)
infer(env, term)
infer(env, context, arg3)
transitive_dependencies(env, name)
trust_report(env, name)
validate_env(env)

Types

result()

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

Functions

add_axiom(env, name, type, universe_params \\ [])

add_constant(env, name, type, universe_params \\ [], opts \\ [])

add_definition(env, name, type, value, universe_params \\ [], opts \\ [])

add_inductive(env, spec)

add_matcher(env, spec)

add_theorem(env, name, type, proof, universe_params \\ [])

axioms(env, name)

check(env, term, expected)

check(env, context, lam, expected)

dependencies(env, name)

infer(env, term)

infer(env, context, arg3)

transitive_dependencies(env, name)

trust_report(env, name)

validate_env(env)