Changeset 1603 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Dec 13, 2011, 5:37:40 PM (8 years ago)
Author:
sacerdot
Message:

More proofs ported to new lib.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r1369 r1603  
    22include "common/FrontEndOps.ma".
    33include "common/CostLabel.ma".
    4 include "utilities/lists.ma".
    5 include "utilities/option.ma".
     4include "basics/lists/list.ma".
    65
    76(* TODO: consider making the typing stricter. *)
     
    8281[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
    8382| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    84 | St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
    85 | St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     83| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
     84| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8685| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
    8786| St_switch _ _ e _ _ ⇒ expr_vars ? e P
    88 | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
     87| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
    8988| _ ⇒ True
    9089].
Note: See TracChangeset for help on using the changeset viewer.