package rapanui.core;

/**
 * Finds justifications for formulas matching given @see FormulaTemplate instances.
 */
public interface JustificationFinder {
	/**
	 * Asynchronously finds justifications that match the template and emits them via the returned emitter.
	 *
	 * @param environment The environment which can be used for justifications. Guaranteed to be non-null.
	 * @param formulaTemplate Describes the kind of formulas that should be justified. Guaranteed to be non-null.
	 * @param recursionDepth The maximum number of recursion levels. Guaranteed to be non-null.
	 *
	 * @return An emitter that emits a new justification whenever it finds one. Must not be null.
	 */
	Emitter<Justification> justifyAsync(ProofEnvironment environment, FormulaTemplate formulaTemplate, int recursionDepth);
}

@@ -16,16 +16,45 @@
 .core;%0A%0A
+import rapanui.dsl.Formula;%0A%0A
 /**%0A * F
@@ -776,24 +776,16 @@
  Formula
-Template
  formula

Modify JustificationFinder: use Formula instead of FormulaTemplate