Theoria.Rewrite (theoria v0.3.0)

Experimental/internal API for 0.2; subject to change before 0.3. Untrusted structural rewrite helpers over core terms.

Summary

direction()

Returns a rewrite direction atom after validation.

Rewrites the first structural occurrence described by an equality term.

Rewrites the first occurrence matched by a possibly schematic rewrite rule.

@type direction() :: :forward | :backward

@spec direction!(direction()) :: direction()

Returns a rewrite direction atom after validation.

@spec once(Theoria.Term.t(), Theoria.Term.Eq.t(), keyword()) ::
  {:ok, Theoria.Term.t()} | :not_found

Rewrites the first structural occurrence described by an equality term.

@spec once_rule(Theoria.Term.t(), Theoria.Rewrite.Rule.t()) ::
  {:ok, Theoria.Term.t()} | :not_found

Rewrites the first occurrence matched by a possibly schematic rewrite rule.