Changeset 737 for src/RTLabs/test


Ignore:
Timestamp:
Apr 4, 2011, 5:13:09 PM (9 years ago)
Author:
campbell
Message:

Use more abstract identifiers in Clight / RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/test/search.ma

    r731 r737  
    4747  definition search1 := 1.
    4848  definition search0 := 0.
    49   definition C_cost0 := ident_of_nat 8.
    50   definition C_cost1 := ident_of_nat 7.
    51   definition C_cost8 := ident_of_nat 6.
    52   definition C_cost6 := ident_of_nat 5.
    53   definition C_cost7 := ident_of_nat 4.
    54   definition C_cost4 := ident_of_nat 3.
    55   definition C_cost5 := ident_of_nat 2.
    56   definition C_cost2 := ident_of_nat 1.
    57   definition C_cost3 := ident_of_nat 0.
     49  definition C_cost0 := costlabel_of_nat 8.
     50  definition C_cost1 := costlabel_of_nat 7.
     51  definition C_cost8 := costlabel_of_nat 6.
     52  definition C_cost6 := costlabel_of_nat 5.
     53  definition C_cost7 := costlabel_of_nat 4.
     54  definition C_cost4 := costlabel_of_nat 3.
     55  definition C_cost5 := costlabel_of_nat 2.
     56  definition C_cost2 := costlabel_of_nat 1.
     57  definition C_cost3 := costlabel_of_nat 0.
    5858
    5959
     
    154154  definition main1 := 1.
    155155  definition main0 := 0.
    156   definition C_cost9 := ident_of_nat 0.
     156  definition C_cost9 := costlabel_of_nat 0.
    157157
    158158
     
    229229   normalize  (* you can examine the result here *)
    230230   % qed.
    231 
Note: See TracChangeset for help on using the changeset viewer.