Theoria.Env (theoria v0.6.0)

Copy Markdown View Source

Kernel environment containing checked constants and definitions.

Summary

Types

name()
t()

Functions

constructor?(env, name)
declarations(env)

Returns declaration names in insertion order.

fetch(env, name)
fetch_constructor(env, name)
fetch_inductive(env, name)
fetch_matcher(env, name)
fetch_recursor(env, name)
inductive?(env, name)
matcher?(env, name)
matchers(env)

Returns matcher declarations in insertion order.

new()
put_axiom(env, name, type, universe_params \\ [])
put_constant(env, name, type, universe_params \\ [], opts \\ [])
put_definition(env, name, type, value, universe_params \\ [], opts \\ [])
put_matcher(env, name, type, value, universe_params \\ [], metadata)
put_theorem(env, name, type, proof, universe_params \\ [])
recursor?(env, name)

Types

name()

@type name() :: atom() | struct()

t()

@type t() :: %Theoria.Env{
  constants: %{required(name()) => Theoria.Env.Constant.t()},
  declarations: [name()]
}

Functions

constructor?(env, name)

@spec constructor?(t(), atom()) :: boolean()

declarations(env)

@spec declarations(t()) :: [name()]

Returns declaration names in insertion order.

fetch(env, name)

@spec fetch(t(), name()) :: {:ok, Theoria.Env.Constant.t()} | :error

fetch_constructor(env, name)

@spec fetch_constructor(t(), atom()) :: {:ok, Theoria.Env.Constructor.t()} | :error

fetch_inductive(env, name)

@spec fetch_inductive(t(), atom()) :: {:ok, Theoria.Env.Inductive.t()} | :error

fetch_matcher(env, name)

@spec fetch_matcher(t(), atom()) :: {:ok, Theoria.Env.Matcher.t()} | :error

fetch_recursor(env, name)

@spec fetch_recursor(t(), atom()) :: {:ok, Theoria.Env.Recursor.t()} | :error

inductive?(env, name)

@spec inductive?(t(), atom()) :: boolean()

matcher?(env, name)

@spec matcher?(t(), atom()) :: boolean()

matchers(env)

@spec matchers(t()) :: [Theoria.Env.Matcher.t()]

Returns matcher declarations in insertion order.

new()

@spec new() :: t()

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

@spec put_axiom(t(), atom(), Theoria.Term.t(), [atom()]) :: t()

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

@spec put_constant(t(), atom(), Theoria.Term.t(), [atom()], keyword()) :: t()

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

@spec put_definition(
  t(),
  atom(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  [atom()],
  keyword()
) :: t()

put_matcher(env, name, type, value, universe_params \\ [], metadata)

@spec put_matcher(
  t(),
  atom(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  [atom()],
  Theoria.Env.Matcher.t()
) ::
  t()

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

@spec put_theorem(t(), atom(), Theoria.Term.t(), Theoria.Term.t(), [atom()]) :: t()

recursor?(env, name)

@spec recursor?(t(), atom()) :: boolean()