Revision dccec723
Added by LĂ©lio Brun over 3 years ago
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
a version that almost work for the k-inuctive two_counters example