Changeset 1250 for src/LIN


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (8 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/LIN/LIN.ma

    r1246 r1250  
    1919definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
    2020
    21 (*CSC: move elsewhere, also in joint/semantics.ma *)
    22 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    23  λA,P,c. match c with [ dp w _ ⇒ w ].
    24 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    25 
    2621definition lin_params: ∀globals. params globals ≝
    2722 λglobals.
Note: See TracChangeset for help on using the changeset viewer.