Theoria.Library.Vec (theoria v0.5.0)

Length-indexed vectors.

Summary

Functions

env()

Returns a new Nat environment extended with Vec declarations.

env_with_indexed_matcher(opts \\ [])

Returns a Vec environment extended with the experimental indexed matcher declaration.

extend(env)

Extends an environment with Vec declarations. Requires Nat declarations.

extend_with_indexed_matcher(env, opts \\ [])

Extends a Vec environment with the experimental indexed matcher declaration.

indexed_matcher_info(matcher_name \\ :vec_match)

Returns equation metadata for the experimental Vec indexed matcher declaration.

inductive_spec()

Returns the inductive specification described by this library.

install_indexed_matcher_equations(package)

Installs realized equation theorems for an experimental indexed matcher package.

Functions

env()

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

Returns a new Nat environment extended with Vec declarations.

env_with_indexed_matcher(opts \\ [])

@spec env_with_indexed_matcher(keyword()) :: {:ok, Theoria.Env.t()} | {:error, term()}

Returns a Vec environment extended with the experimental indexed matcher declaration.

extend(env)

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

Extends an environment with Vec declarations. Requires Nat declarations.

extend_with_indexed_matcher(env, opts \\ [])

@spec extend_with_indexed_matcher(
  Theoria.Env.t(),
  keyword()
) :: {:ok, Theoria.Env.t()} | {:error, term()}

Extends a Vec environment with the experimental indexed matcher declaration.

indexed_matcher_info(matcher_name \\ :vec_match)

@spec indexed_matcher_info(atom()) :: Theoria.Equation.Info.t()

Returns equation metadata for the experimental Vec indexed matcher declaration.

inductive_spec()

@spec inductive_spec() :: Theoria.Inductive.Spec.t()

Returns the inductive specification described by this library.

install_indexed_matcher_equations(package)

@spec install_indexed_matcher_equations(Theoria.Equation.Matcher.Indexed.Package.t()) ::
  {:ok, Theoria.Env.t(), [Theoria.Theorem.t()]} | {:error, term()}

Installs realized equation theorems for an experimental indexed matcher package.