Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

src/machine_code_types.mli
60 60
type mc_contract_t = {
61 61
  mc_pre: mc_formula_t;
62 62
  mc_post: mc_formula_t;
63
  mc_proof: proof_annotation option
63 64
}
64 65

  
65 66
type machine_spec = {

Also available in: Unified diff