Ignore:
Timestamp:
Dec 19, 2012, 10:38:43 AM (8 years ago)
Author:
piccolo
Message:

linearise modified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2561 r2562  
    153153
    154154inductive call_kind : Type[0] ≝
    155 | call_ptr : call_kind
    156 | call_id : call_kind.
     155| PTR : call_kind
     156| ID : call_kind.
    157157
    158158definition kind_of_call :
    159159  ∀p.(ident + (dpl_arg p × (dph_arg p))) → call_kind ≝
    160   λp,f.match f with [ inl _ ⇒ call_id | inr _ ⇒ call_ptr ].
     160  λp,f.match f with [ inl _ ⇒ ID | inr _ ⇒ PTR ].
    161161
    162162record sem_unserialized_params
Note: See TracChangeset for help on using the changeset viewer.