public interface ProofVerifier
Refer to mmj.verify.ProofConstants.java for information about proof parameters and error messages.
Modifier and Type | Method and Description |
---|---|
void |
verifyAllExprRPNAsProofs(Messages messages,
java.util.Map<java.lang.String,Stmt> stmtTbl)
Verify all Statements' grammatical parse RPNs.
|
void |
verifyAllProofs(Messages messages,
java.util.Map<java.lang.String,Stmt> stmtTbl)
Verify all proofs in Statement Table.
|
VerifyException |
verifyExprRPNAsProof(Stmt exprRPNStmt)
Verify grammatical parse RPN as if it were a proof.
|
VerifyException |
verifyOneProof(Theorem theorem)
Verify a single proof.
|
VerifyException verifyOneProof(Theorem theorem)
theorem
- Theorem object reference.void verifyAllProofs(Messages messages, java.util.Map<java.lang.String,Stmt> stmtTbl)
messages
- Messages object for output error messages.stmtTbl
- Statement Table (map).VerifyException verifyExprRPNAsProof(Stmt exprRPNStmt)
Note: even VarHyp and Syntax Axioms are assigned default RPN's, so this should work -- unless there are errors in the Metamath file, or in the grammar itself.
exprRPNStmt
- Stmt with RPN to verify.void verifyAllExprRPNAsProofs(Messages messages, java.util.Map<java.lang.String,Stmt> stmtTbl)
Note: even VarHyp and Syntax Axioms are assigned default RPN's, so this should work -- unless there are errors in the Metamath file, or in the grammar itself.
messages
- Messages object for output error messages.stmtTbl
- Statement Table (map).