Ignore:
Timestamp:
Dec 19, 2011, 2:48:33 PM (8 years ago)
Author:
campbell
Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1610 r1626  
    2121(* None of the additional code introduces locals or labels. *)
    2222definition stmt_inv : stmt → Prop ≝
    23   stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     23  stmt_P (λs. stmt_vars (λ_.λ_.False) s ∧ stmt_labels (λ_.False) s).
    2424 
    2525discriminator option.
     
    9797[ % [ % // |
    9898  @(stmt_P_mp … H) #s * #V #L %
    99   [ @(stmt_vars_mp … V) #i *
     99  [ @(stmt_vars_mp … V) #i #t *
    100100  | @(stmt_labels_mp … L) #l *
    101101  ]
Note: See TracChangeset for help on using the changeset viewer.