Experimental/internal API for 0.2; subject to change before 0.3. Statement planning for matcher equations.
Summary
Functions
Builds an indexed matcher equation theorem statement.
Builds indexed matcher equation statements for every equation.
Turns planned indexed matcher equation statement metadata into lemma metadata.
Functions
@spec indexed(term(), Theoria.Equation.Matcher.Equation.t()) :: {:ok, Theoria.Term.t()} | {:error, term()}
Builds an indexed matcher equation theorem statement.
@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.
@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.