Changeset 2773 for extracted/z.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/z.ml

    r2743 r2773  
    2626let rec z_rect_Type4 h_OZ h_pos h_neg = function
    2727| OZ -> h_OZ
    28 | Pos x_4734 -> h_pos x_4734
    29 | Neg x_4735 -> h_neg x_4735
     28| Pos x_1375 -> h_pos x_1375
     29| Neg x_1376 -> h_neg x_1376
    3030
    3131(** val z_rect_Type5 :
     
    3333let rec z_rect_Type5 h_OZ h_pos h_neg = function
    3434| OZ -> h_OZ
    35 | Pos x_4740 -> h_pos x_4740
    36 | Neg x_4741 -> h_neg x_4741
     35| Pos x_1381 -> h_pos x_1381
     36| Neg x_1382 -> h_neg x_1382
    3737
    3838(** val z_rect_Type3 :
     
    4040let rec z_rect_Type3 h_OZ h_pos h_neg = function
    4141| OZ -> h_OZ
    42 | Pos x_4746 -> h_pos x_4746
    43 | Neg x_4747 -> h_neg x_4747
     42| Pos x_1387 -> h_pos x_1387
     43| Neg x_1388 -> h_neg x_1388
    4444
    4545(** val z_rect_Type2 :
     
    4747let rec z_rect_Type2 h_OZ h_pos h_neg = function
    4848| OZ -> h_OZ
    49 | Pos x_4752 -> h_pos x_4752
    50 | Neg x_4753 -> h_neg x_4753
     49| Pos x_1393 -> h_pos x_1393
     50| Neg x_1394 -> h_neg x_1394
    5151
    5252(** val z_rect_Type1 :
     
    5454let rec z_rect_Type1 h_OZ h_pos h_neg = function
    5555| OZ -> h_OZ
    56 | Pos x_4758 -> h_pos x_4758
    57 | Neg x_4759 -> h_neg x_4759
     56| Pos x_1399 -> h_pos x_1399
     57| Neg x_1400 -> h_neg x_1400
    5858
    5959(** val z_rect_Type0 :
     
    6161let rec z_rect_Type0 h_OZ h_pos h_neg = function
    6262| OZ -> h_OZ
    63 | Pos x_4764 -> h_pos x_4764
    64 | Neg x_4765 -> h_neg x_4765
     63| Pos x_1405 -> h_pos x_1405
     64| Neg x_1406 -> h_neg x_1406
    6565
    6666(** val z_inv_rect_Type4 :
     
    131131  (match n with
    132132   | Positive.One -> OZ
    133    | Positive.P1 x -> Neg (Positive.pred0 n)
    134    | Positive.P0 x -> Neg (Positive.pred0 n))
     133   | Positive.P1 x -> Neg (Positive.pred n)
     134   | Positive.P0 x -> Neg (Positive.pred n))
    135135
    136136(** val zpred : z -> z **)
     
    140140  (match n with
    141141   | Positive.One -> OZ
    142    | Positive.P1 x -> Pos (Positive.pred0 n)
    143    | Positive.P0 x -> Pos (Positive.pred0 n))
     142   | Positive.P1 x -> Pos (Positive.pred n)
     143   | Positive.P0 x -> Pos (Positive.pred n))
    144144| Neg n -> Neg (Positive.succ n)
    145 
    146 type zle = __
    147 
    148 type zlt = __
    149145
    150146(** val eqZb : z -> z -> Bool.bool **)
     
    159155    (match y with
    160156     | OZ -> Bool.False
    161      | Pos q -> Positive.eqb0 p q
     157     | Pos q -> Positive.eqb p q
    162158     | Neg q -> Bool.False)
    163159  | Neg p ->
     
    165161     | OZ -> Bool.False
    166162     | Pos q -> Bool.False
    167      | Neg q -> Positive.eqb0 p q)
     163     | Neg q -> Positive.eqb p q)
    168164
    169165(** val z_compare : z -> z -> Positive.compare **)
     
    193189    (match y with
    194190     | OZ -> x
    195      | Pos n -> Pos (Positive.plus0 m n)
     191     | Pos n -> Pos (Positive.plus m n)
    196192     | Neg n ->
    197193       (match Positive.pos_compare m n with
    198         | Positive.LT -> Neg (Positive.minus0 n m)
     194        | Positive.LT -> Neg (Positive.minus n m)
    199195        | Positive.EQ -> OZ
    200         | Positive.GT -> Pos (Positive.minus0 m n)))
     196        | Positive.GT -> Pos (Positive.minus m n)))
    201197  | Neg m ->
    202198    (match y with
     
    204200     | Pos n ->
    205201       (match Positive.pos_compare m n with
    206         | Positive.LT -> Pos (Positive.minus0 n m)
     202        | Positive.LT -> Pos (Positive.minus n m)
    207203        | Positive.EQ -> OZ
    208         | Positive.GT -> Neg (Positive.minus0 m n))
    209      | Neg n -> Neg (Positive.plus0 m n))
     204        | Positive.GT -> Neg (Positive.minus m n))
     205     | Neg n -> Neg (Positive.plus m n))
    210206
    211207(** val zopp : z -> z **)
     
    252248    (match y with
    253249     | OZ -> Bool.False
    254      | Pos m -> Positive.leb0 n m
     250     | Pos m -> Positive.leb n m
    255251     | Neg m -> Bool.False)
    256252  | Neg n ->
     
    258254     | OZ -> Bool.True
    259255     | Pos m -> Bool.True
    260      | Neg m -> Positive.leb0 m n)
     256     | Neg m -> Positive.leb m n)
    261257
    262258(** val zltb : z -> z -> Bool.bool **)
     
    271267    (match y with
    272268     | OZ -> Bool.False
    273      | Pos m -> Positive.leb0 (Positive.succ n) m
     269     | Pos m -> Positive.leb (Positive.succ n) m
    274270     | Neg m -> Bool.False)
    275271  | Neg n ->
     
    277273     | OZ -> Bool.True
    278274     | Pos m -> Bool.True
    279      | Neg m -> Positive.leb0 (Positive.succ m) n)
     275     | Neg m -> Positive.leb (Positive.succ m) n)
    280276
    281277(** val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     
    294290    (match y with
    295291     | OZ -> OZ
    296      | Pos m -> Pos (Positive.times0 n m)
    297      | Neg m -> Neg (Positive.times0 n m))
     292     | Pos m -> Pos (Positive.times n m)
     293     | Neg m -> Neg (Positive.times n m))
    298294  | Neg n ->
    299295    (match y with
    300296     | OZ -> OZ
    301      | Pos m -> Neg (Positive.times0 n m)
    302      | Neg m -> Pos (Positive.times0 n m))
     297     | Pos m -> Neg (Positive.times n m)
     298     | Neg m -> Pos (Positive.times n m))
    303299
    304300(** val zmax : z -> z -> z **)
Note: See TracChangeset for help on using the changeset viewer.