Ignore:
Timestamp:
Mar 30, 2011, 4:16:08 PM (9 years ago)
Author:
campbell
Message:

Do some light manual disambiguation to make Clight examples go through more
easily.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/transform1.ma

    r717 r725  
    1919ndefinition skippy_fd : fundef → fundef ≝ λf.
    2020match f with
    21 [ Internal fd ⇒ Internal (skippy_f fd)
    22 | External id args res ⇒ External id args res
     21[ CL_Internal fd ⇒ Internal (skippy_f fd)
     22| CL_External id args res ⇒ External id args res
    2323].
    2424
     
    3131mk_program ??
    3232  (map ?? (λfd. match snd ?? fd with
    33              [ Internal f ⇒
     33             [ CL_Internal f ⇒
    3434               〈fst ?? fd,
    35                 Internal
     35                CL_Internal
    3636                 (mk_function (fn_return f) (fn_params f) (fn_vars f) (skippy_s (fn_body f)))〉
    37              | External _ _ _ ⇒ fd ])
     37             | CL_External _ _ _ ⇒ fd ])
    3838    (prog_funct ?? p))
    3939  (prog_main ?? p)
Note: See TracChangeset for help on using the changeset viewer.