Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/corelang.mli | ||
---|---|---|
271 | 271 |
val mk_contract_var : |
272 | 272 |
ident -> bool -> type_dec option -> expr -> Location.t -> contract_desc |
273 | 273 |
|
274 |
val mk_contract_guarantees : string option -> eexpr -> contract_desc |
|
274 |
val mk_contract_guarantees : string option -> eexpr -> proof_annotation option -> contract_desc
|
|
275 | 275 |
|
276 | 276 |
val mk_contract_assume : string option -> eexpr -> contract_desc |
277 | 277 |
|
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example