Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/lustre_types.mli | ||
---|---|---|
140 | 140 |
hand_loc : Location.t; |
141 | 141 |
} |
142 | 142 |
|
143 |
type proof_annotation = Kinduction of int |
|
144 |
|
|
143 | 145 |
type contract_desc = { |
144 | 146 |
consts : var_decl list; |
145 | 147 |
locals : var_decl list; |
... | ... | |
149 | 151 |
modes : contract_mode list; |
150 | 152 |
imports : contract_import list; |
151 | 153 |
spec_loc : Location.t; |
154 |
proof : proof_annotation option |
|
152 | 155 |
} |
153 | 156 |
|
154 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident * 'a option
|
|
157 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident |
|
155 | 158 |
|
156 | 159 |
type node_desc = { |
157 | 160 |
node_id : ident; |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example