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/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