public interface Prover
prove(WorksheetInfo, ParseNode)
method describes one stage of this,
with an input goal and output an assrt and a list of subgoals.Modifier and Type | Interface and Description |
---|---|
static class |
Prover.AssrtProver
A general interface for specifying reverse provers, which start at the
goal and work backwards producing Assrts as they go.
|
static class |
Prover.HypProver
An extension to
Prover , where the function is only required to
give an Assrt and substitutions to the variables in the Assrt. |
static class |
Prover.HypProverResult
Result type for a
Prover.HypProver . |
static class |
Prover.ProverResult |
Modifier and Type | Method and Description |
---|---|
Prover.ProverResult |
prove(mmj.transforms.WorksheetInfo info,
ParseNode root)
Prove the given expression from scratch.
|
Prover.ProverResult prove(mmj.transforms.WorksheetInfo info, ParseNode root)
null
if this prover doesn't know how to prove the theorem
using its assrt, or the list of hypothesis subgoals that result.info
- The contextroot
- The goal expression