Theoria.Equation.Matcher.Statement (theoria v0.3.0)

Copy Markdown View Source

Experimental/internal API for 0.2; subject to change before 0.3. Statement planning for matcher equations.

Summary

Functions

indexed(shape, equation)

Builds an indexed matcher equation theorem statement.

indexed_all(shape, equations)

Builds indexed matcher equation statements for every equation.

indexed_to_lemma(equation)

Turns planned indexed matcher equation statement metadata into lemma metadata.

Functions

indexed(shape, equation)

@spec indexed(term(), Theoria.Equation.Matcher.Equation.t()) ::
  {:ok, Theoria.Term.t()} | {:error, term()}

Builds an indexed matcher equation theorem statement.

indexed_all(shape, equations)

@spec indexed_all(term(), [Theoria.Equation.Matcher.Equation.t()]) ::
  {:ok, [Theoria.Equation.Matcher.Equation.t()]} | {:error, term()}

Builds indexed matcher equation statements for every equation.

indexed_to_lemma(equation)

@spec indexed_to_lemma(Theoria.Equation.Matcher.Equation.t()) ::
  {:ok, Theoria.Equation.Lemma.t()} | {:error, term()}

Turns planned indexed matcher equation statement metadata into lemma metadata.