Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (9 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1247 r1250  
    205205axiom FailedLoad : String.
    206206axiom BadFunction : String.
    207 
    208 (*CSC: move elsewhere, also in LIN.ma *)
    209 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    210  λA,P,c. match c with [ dp w _ ⇒ w ].
    211 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    212207
    213208definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
Note: See TracChangeset for help on using the changeset viewer.