Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/lustre_types.ml | ||
---|---|---|
151 | 151 |
hand_loc : Location.t; |
152 | 152 |
} |
153 | 153 |
|
154 |
type proof_annotation = Kinduction of int |
|
155 |
|
|
154 | 156 |
type contract_desc = { |
155 | 157 |
consts : var_decl list; |
156 | 158 |
locals : var_decl list; |
... | ... | |
160 | 162 |
modes : contract_mode list; |
161 | 163 |
imports : contract_import list; |
162 | 164 |
spec_loc : Location.t; |
165 |
proof : proof_annotation option |
|
163 | 166 |
} |
164 | 167 |
|
165 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident * 'a option
|
|
168 |
type 'a node_spec_t = Contract of 'a | NodeSpec of ident |
|
166 | 169 |
|
167 | 170 |
type node_desc = { |
168 | 171 |
node_id : ident; |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example