Theoria.Equation.Lemma (theoria v0.3.0)

Experimental/internal API for 0.2; subject to change before 0.3. Metadata for an equation lemma generated from compiled equations.

Summary

Types

binder()

t()

Functions

add_all_to_env(env, lemmas, equality_or_opts \\ [], opts \\ [])

Kernel-checks and installs many equation lemmas as opaque theorem declarations.

add_generated_to_env(env, equation, opts \\ [])

Kernel-checks and installs generated equation lemmas for a supported definition.

add_to_env(env, lemma, equality_or_opts \\ [], opts \\ [])

Kernel-checks and installs equation-lemma metadata as an opaque theorem declaration.

defeq_check(lemma, category)

Turns equation-lemma metadata into a native definitional-equality validation check.

defeq_checks(category, lemmas)

Turns many equation lemmas into native definitional-equality validation checks.

for_definition(info, suffix, left, right, opts \\ [])

Builds equation-lemma metadata named after a compiled definition.

generated_for(info, opts \\ [])

Generates equation lemmas from stored equation schema metadata.

new(name_or_id, left, right, opts \\ [])

Builds equation-lemma metadata.

realize(env, lemma, equality_or_opts \\ [], opts \\ [])

Kernel-checks equation-lemma metadata as an anonymous generated equation artifact.

theorem_name(definition_name, suffix)

Returns the Lean-style theorem name for a definition equation.

to_theorem(env, lemma, equality_or_opts \\ [], opts \\ [])

Kernel-checks equation-lemma metadata as a theorem using reflexivity.

unfold_for(info)

Generates an unfolding equation lemma for a stored equation definition.

Types

binder()

@type binder() :: {atom(), Theoria.Term.t()}

t()

@type t() :: %Theoria.Equation.Lemma{
  binders: [binder()],
  equality_type: Theoria.Term.t() | nil,
  identity: Theoria.Equation.Identity.t() | nil,
  left: Theoria.Term.t(),
  name: atom() | Theoria.Equation.Identity.t(),
  right: Theoria.Term.t(),
  source: Theoria.Equation.Clause.t() | nil
}

Functions

add_all_to_env(env, lemmas, equality_or_opts \\ [], opts \\ [])

@spec add_all_to_env(Theoria.Env.t(), [t()], Theoria.Term.t() | keyword(), keyword()) ::
  {:ok, Theoria.Env.t(), [Theoria.Theorem.t()]} | {:error, Theoria.Error.t()}

Kernel-checks and installs many equation lemmas as opaque theorem declarations.

add_generated_to_env(env, equation, opts \\ [])

@spec add_generated_to_env(
  Theoria.Env.t(),
  atom() | Theoria.Equation.Info.t(),
  keyword()
) ::
  {:ok, Theoria.Env.t(), [Theoria.Theorem.t()]} | {:error, term()}

Kernel-checks and installs generated equation lemmas for a supported definition.

add_to_env(env, lemma, equality_or_opts \\ [], opts \\ [])

@spec add_to_env(Theoria.Env.t(), t(), Theoria.Term.t() | keyword(), keyword()) ::
  {:ok, Theoria.Env.t(), Theoria.Theorem.t()} | {:error, Theoria.Error.t()}

Kernel-checks and installs equation-lemma metadata as an opaque theorem declaration.

defeq_check(lemma, category)

@spec defeq_check(t(), atom()) :: Theoria.Validation.DefeqCheck.t()

Turns equation-lemma metadata into a native definitional-equality validation check.

defeq_checks(category, lemmas)

@spec defeq_checks(atom(), [t()]) :: [Theoria.Validation.DefeqCheck.t()]

Turns many equation lemmas into native definitional-equality validation checks.

for_definition(info, suffix, left, right, opts \\ [])

@spec for_definition(
  Theoria.Equation.Info.t(),
  atom(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  keyword()
) ::
  t()

Builds equation-lemma metadata named after a compiled definition.

generated_for(info, opts \\ [])

@spec generated_for(
  Theoria.Equation.Info.t(),
  keyword()
) :: [t()]

Generates equation lemmas from stored equation schema metadata.

new(name_or_id, left, right, opts \\ [])

@spec new(
  atom() | Theoria.Equation.Identity.t(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  keyword()
) :: t()

Builds equation-lemma metadata.

realize(env, lemma, equality_or_opts \\ [], opts \\ [])

@spec realize(Theoria.Env.t(), t(), Theoria.Term.t() | keyword(), keyword()) ::
  {:ok, Theoria.Equation.Realized.t()} | {:error, Theoria.Error.t()}

Kernel-checks equation-lemma metadata as an anonymous generated equation artifact.

theorem_name(definition_name, suffix)

@spec theorem_name(atom(), atom()) :: Theoria.Equation.Identity.t()

Returns the Lean-style theorem name for a definition equation.

to_theorem(env, lemma, equality_or_opts \\ [], opts \\ [])

@spec to_theorem(Theoria.Env.t(), t(), Theoria.Term.t() | keyword(), keyword()) ::
  {:ok, Theoria.Theorem.t()} | {:error, Theoria.Error.t()}

Kernel-checks equation-lemma metadata as a theorem using reflexivity.

unfold_for(info)

@spec unfold_for(Theoria.Equation.Info.t()) :: t()

Generates an unfolding equation lemma for a stored equation definition.