Theoria.Rewrite.Rule (theoria v0.4.0)

Experimental/internal API for 0.2; subject to change before 0.3. A theorem-like rewrite rule over a core equality term.

Summary

Types

t()

Functions

from_lemma(lemma, equality_or_opts \\ [], opts \\ [])

Builds a rewrite rule from equation-lemma metadata.

from_realized(realized)

Builds a rewrite rule from a realized equation artifact.

from_realizing_lemma(env, lemma, opts \\ [])

Builds a rewrite rule from equation-lemma metadata, realizing it first when requested.

new(name_or_id, equality, opts \\ [])

Builds a rewrite rule.

realize(env, rule, opts \\ [])

Realizes a lazy proof-backed rewrite rule.

Types

t()

@type t() :: %Theoria.Rewrite.Rule{
  binders: [Theoria.Equation.Lemma.binder()],
  direction: :forward | :backward,
  equality: Theoria.Term.Eq.t(),
  identity: Theoria.Equation.Identity.t() | nil,
  name: atom() | Theoria.Equation.Identity.t(),
  proof: Theoria.Term.t() | nil,
  realize: false | true | :lazy,
  realized: Theoria.Equation.Realized.t() | nil,
  source_lemma: Theoria.Equation.Lemma.t() | nil
}

Functions

from_lemma(lemma, equality_or_opts \\ [], opts \\ [])

@spec from_lemma(Theoria.Equation.Lemma.t(), Theoria.Term.t() | keyword(), keyword()) ::
  t()

Builds a rewrite rule from equation-lemma metadata.

from_realized(realized)

@spec from_realized(Theoria.Equation.Realized.t()) :: t()

Builds a rewrite rule from a realized equation artifact.

from_realizing_lemma(env, lemma, opts \\ [])

@spec from_realizing_lemma(Theoria.Env.t(), Theoria.Equation.Lemma.t(), keyword()) ::
  t()

Builds a rewrite rule from equation-lemma metadata, realizing it first when requested.

new(name_or_id, equality, opts \\ [])

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

Builds a rewrite rule.

realize(env, rule, opts \\ [])

@spec realize(Theoria.Env.t(), t(), keyword()) :: t()

Realizes a lazy proof-backed rewrite rule.