public abstract static class Prover.HypProver extends Prover.AssrtProver
Prover
, where the function is only required to
give an Assrt and substitutions to the variables in the Assrt.Prover.AssrtProver, Prover.HypProver, Prover.HypProverResult, Prover.ProverResult
assrt
Modifier and Type | Method and Description |
---|---|
abstract Prover.HypProverResult |
hypProve(mmj.transforms.WorksheetInfo info,
ParseNode root)
Similar to
Prover.prove(WorksheetInfo, ParseNode) . |
Prover.ProverResult |
prove(mmj.transforms.WorksheetInfo info,
ParseNode root)
Prove the given expression from scratch.
|
toString
public HypProver(Assrt assrt)
public abstract Prover.HypProverResult hypProve(mmj.transforms.WorksheetInfo info, ParseNode root)
Prover.prove(WorksheetInfo, ParseNode)
. Prove a
goal expression, producing an Assrt and a list of substitutions to
variables. The list of variables must be exhaustive in all VarHyps
used in the conclusion and its hypotheses; failure to do so will
cause an IllegalArgumentException
.info
- The contextroot
- The goal expressionpublic Prover.ProverResult prove(mmj.transforms.WorksheetInfo info, ParseNode root)
Prover
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