Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/positiveMap.ml

    r2775 r2797  
    4444let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
    4545| Pm_leaf -> h_pm_leaf
    46 | Pm_node (x_3157, x_3156, x_3155) ->
    47   h_pm_node x_3157 x_3156 x_3155
    48     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3156)
    49     (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3155)
     46| Pm_node (x_3170, x_3169, x_3168) ->
     47  h_pm_node x_3170 x_3169 x_3168
     48    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3169)
     49    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3168)
    5050
    5151(** val positive_map_rect_Type3 :
     
    5454let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
    5555| Pm_leaf -> h_pm_leaf
    56 | Pm_node (x_3169, x_3168, x_3167) ->
    57   h_pm_node x_3169 x_3168 x_3167
    58     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3168)
    59     (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3167)
     56| Pm_node (x_3182, x_3181, x_3180) ->
     57  h_pm_node x_3182 x_3181 x_3180
     58    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3181)
     59    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3180)
    6060
    6161(** val positive_map_rect_Type2 :
     
    6464let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
    6565| Pm_leaf -> h_pm_leaf
    66 | Pm_node (x_3175, x_3174, x_3173) ->
    67   h_pm_node x_3175 x_3174 x_3173
    68     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3174)
    69     (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3173)
     66| Pm_node (x_3188, x_3187, x_3186) ->
     67  h_pm_node x_3188 x_3187 x_3186
     68    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3187)
     69    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3186)
    7070
    7171(** val positive_map_rect_Type1 :
     
    7474let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
    7575| Pm_leaf -> h_pm_leaf
    76 | Pm_node (x_3181, x_3180, x_3179) ->
    77   h_pm_node x_3181 x_3180 x_3179
    78     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3180)
    79     (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3179)
     76| Pm_node (x_3194, x_3193, x_3192) ->
     77  h_pm_node x_3194 x_3193 x_3192
     78    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3193)
     79    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3192)
    8080
    8181(** val positive_map_rect_Type0 :
     
    8484let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
    8585| Pm_leaf -> h_pm_leaf
    86 | Pm_node (x_3187, x_3186, x_3185) ->
    87   h_pm_node x_3187 x_3186 x_3185
    88     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3186)
    89     (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3185)
     86| Pm_node (x_3200, x_3199, x_3198) ->
     87  h_pm_node x_3200 x_3199 x_3198
     88    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3199)
     89    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3198)
    9090
    9191(** val positive_map_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.