Overview  Index  Help 

PROOF_CHECKER

All Known Implementing Modules:

ProofChecker


The First-Order LoopW Proof Checker proof checking. The proof checker verify that the given program respresents a correct proof.

           
Value summary

val checkClosedProg : ProofAst.program -> bool
           check that the given program represents a correct proof.

 

       
Value detail

checkClosedProg

fun checkClosedProg p : ProofAst.program -> bool

check that the given program represents a correct proof.

Parameters:
p
the program.
Returns:
true if and only if p is a correct proof.

 


Overview  Index  Help