Exported names:
- Operations:
- addPreConditions
- verifyPostConditions
- verifyPreConditions
Imported modules:

Module ContractProver

Summary of exported operations:

verifyPostConditions
                  ::  AProg TypeExpr -> StateT VState IO (AProg TypeExpr)

verifyPreConditions
                  ::  AProg TypeExpr -> StateT VState IO (AProg TypeExpr)

addPreConditions
                  ::  AProg TypeExpr -> StateT VState IO (AProg TypeExpr)

Deterministic

Exported operations:

verifyPostConditions :: AProg TypeExpr -> StateT VState IO (AProg TypeExpr)

verifyPreConditions :: AProg TypeExpr -> StateT VState IO (AProg TypeExpr)

addPreConditions :: AProg TypeExpr -> StateT VState IO (AProg TypeExpr)