Changeset 2773 for extracted/positive.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/positive.ml

    r2601 r2773  
    104104let rec pos_rect_Type4 h_one h_p1 h_p0 = function
    105105| One -> h_one
    106 | P1 x_1375 -> h_p1 x_1375 (pos_rect_Type4 h_one h_p1 h_p0 x_1375)
    107 | P0 x_1376 -> h_p0 x_1376 (pos_rect_Type4 h_one h_p1 h_p0 x_1376)
     106| P1 x_1037 -> h_p1 x_1037 (pos_rect_Type4 h_one h_p1 h_p0 x_1037)
     107| P0 x_1038 -> h_p0 x_1038 (pos_rect_Type4 h_one h_p1 h_p0 x_1038)
    108108
    109109(** val pos_rect_Type3 :
     
    111111let rec pos_rect_Type3 h_one h_p1 h_p0 = function
    112112| One -> h_one
    113 | P1 x_1387 -> h_p1 x_1387 (pos_rect_Type3 h_one h_p1 h_p0 x_1387)
    114 | P0 x_1388 -> h_p0 x_1388 (pos_rect_Type3 h_one h_p1 h_p0 x_1388)
     113| P1 x_1049 -> h_p1 x_1049 (pos_rect_Type3 h_one h_p1 h_p0 x_1049)
     114| P0 x_1050 -> h_p0 x_1050 (pos_rect_Type3 h_one h_p1 h_p0 x_1050)
    115115
    116116(** val pos_rect_Type2 :
     
    118118let rec pos_rect_Type2 h_one h_p1 h_p0 = function
    119119| One -> h_one
    120 | P1 x_1393 -> h_p1 x_1393 (pos_rect_Type2 h_one h_p1 h_p0 x_1393)
    121 | P0 x_1394 -> h_p0 x_1394 (pos_rect_Type2 h_one h_p1 h_p0 x_1394)
     120| P1 x_1055 -> h_p1 x_1055 (pos_rect_Type2 h_one h_p1 h_p0 x_1055)
     121| P0 x_1056 -> h_p0 x_1056 (pos_rect_Type2 h_one h_p1 h_p0 x_1056)
    122122
    123123(** val pos_rect_Type1 :
     
    125125let rec pos_rect_Type1 h_one h_p1 h_p0 = function
    126126| One -> h_one
    127 | P1 x_1399 -> h_p1 x_1399 (pos_rect_Type1 h_one h_p1 h_p0 x_1399)
    128 | P0 x_1400 -> h_p0 x_1400 (pos_rect_Type1 h_one h_p1 h_p0 x_1400)
     127| P1 x_1061 -> h_p1 x_1061 (pos_rect_Type1 h_one h_p1 h_p0 x_1061)
     128| P0 x_1062 -> h_p0 x_1062 (pos_rect_Type1 h_one h_p1 h_p0 x_1062)
    129129
    130130(** val pos_rect_Type0 :
     
    132132let rec pos_rect_Type0 h_one h_p1 h_p0 = function
    133133| One -> h_one
    134 | P1 x_1405 -> h_p1 x_1405 (pos_rect_Type0 h_one h_p1 h_p0 x_1405)
    135 | P0 x_1406 -> h_p0 x_1406 (pos_rect_Type0 h_one h_p1 h_p0 x_1406)
     134| P1 x_1067 -> h_p1 x_1067 (pos_rect_Type0 h_one h_p1 h_p0 x_1067)
     135| P0 x_1068 -> h_p0 x_1068 (pos_rect_Type0 h_one h_p1 h_p0 x_1068)
    136136
    137137(** val pos_inv_rect_Type4 :
     
    173173     | P0 a0 -> Obj.magic (fun _ dH -> dH __)) y
    174174
    175 (** val pred0 : pos -> pos **)
    176 let rec pred0 = function
     175(** val pred : pos -> pos **)
     176let rec pred = function
    177177| One -> One
    178178| P1 ps -> P0 ps
     
    180180  (match ps with
    181181   | One -> One
    182    | P1 x -> P1 (pred0 ps)
    183    | P0 x -> P1 (pred0 ps))
     182   | P1 x -> P1 (pred ps)
     183   | P0 x -> P1 (pred ps))
    184184
    185185(** val succ : pos -> pos **)
     
    200200| Nat.S n' -> succ (succ_pos_of_nat n')
    201201
    202 (** val plus0 : pos -> pos -> pos **)
    203 let rec plus0 n m =
     202(** val plus : pos -> pos -> pos **)
     203let rec plus n m =
    204204  match n with
    205205  | One -> succ m
     
    207207    (match m with
    208208     | One -> succ n
    209      | P1 m' -> P0 (succ (plus0 n' m'))
    210      | P0 m' -> P1 (plus0 n' m'))
     209     | P1 m' -> P0 (succ (plus n' m'))
     210     | P0 m' -> P1 (plus n' m'))
    211211  | P0 n' ->
    212212    (match m with
    213213     | One -> P1 n'
    214      | P1 m' -> P1 (plus0 n' m')
    215      | P0 m' -> P0 (plus0 n' m'))
    216 
    217 (** val times0 : pos -> pos -> pos **)
    218 let rec times0 n m =
     214     | P1 m' -> P1 (plus n' m')
     215     | P0 m' -> P0 (plus n' m'))
     216
     217(** val times : pos -> pos -> pos **)
     218let rec times n m =
    219219  match n with
    220220  | One -> m
    221   | P1 n' -> plus0 m (P0 (times0 n' m))
    222   | P0 n' -> P0 (times0 n' m)
     221  | P1 n' -> plus m (P0 (times n' m))
     222  | P0 n' -> P0 (times n' m)
    223223
    224224type minusresult =
     
    232232| MinusNeg -> h_MinusNeg
    233233| MinusZero -> h_MinusZero
    234 | MinusPos x_1582 -> h_MinusPos x_1582
     234| MinusPos x_1244 -> h_MinusPos x_1244
    235235
    236236(** val minusresult_rect_Type5 :
     
    239239| MinusNeg -> h_MinusNeg
    240240| MinusZero -> h_MinusZero
    241 | MinusPos x_1587 -> h_MinusPos x_1587
     241| MinusPos x_1249 -> h_MinusPos x_1249
    242242
    243243(** val minusresult_rect_Type3 :
     
    246246| MinusNeg -> h_MinusNeg
    247247| MinusZero -> h_MinusZero
    248 | MinusPos x_1592 -> h_MinusPos x_1592
     248| MinusPos x_1254 -> h_MinusPos x_1254
    249249
    250250(** val minusresult_rect_Type2 :
     
    253253| MinusNeg -> h_MinusNeg
    254254| MinusZero -> h_MinusZero
    255 | MinusPos x_1597 -> h_MinusPos x_1597
     255| MinusPos x_1259 -> h_MinusPos x_1259
    256256
    257257(** val minusresult_rect_Type1 :
     
    260260| MinusNeg -> h_MinusNeg
    261261| MinusZero -> h_MinusZero
    262 | MinusPos x_1602 -> h_MinusPos x_1602
     262| MinusPos x_1264 -> h_MinusPos x_1264
    263263
    264264(** val minusresult_rect_Type0 :
     
    267267| MinusNeg -> h_MinusNeg
    268268| MinusZero -> h_MinusZero
    269 | MinusPos x_1607 -> h_MinusPos x_1607
     269| MinusPos x_1269 -> h_MinusPos x_1269
    270270
    271271(** val minusresult_inv_rect_Type4 :
     
    325325  | P0 n' ->
    326326    (match m with
    327      | One -> MinusPos (pred0 n)
     327     | One -> MinusPos (pred n)
    328328     | P1 m' ->
    329329       (match partial_minus n' m' with
    330330        | MinusNeg -> MinusNeg
    331331        | MinusZero -> MinusNeg
    332         | MinusPos p -> MinusPos (pred0 (P0 p)))
     332        | MinusPos p -> MinusPos (pred (P0 p)))
    333333     | P0 m' ->
    334334       (match partial_minus n' m' with
     
    337337        | MinusPos p -> MinusPos (P0 p)))
    338338
    339 (** val minus0 : pos -> pos -> pos **)
    340 let minus0 n m =
     339(** val minus : pos -> pos -> pos **)
     340let minus n m =
    341341  match partial_minus n m with
    342342  | MinusNeg -> One
     
    344344  | MinusPos p -> p
    345345
    346 (** val eqb0 : pos -> pos -> Bool.bool **)
    347 let rec eqb0 n m =
     346(** val eqb : pos -> pos -> Bool.bool **)
     347let rec eqb n m =
    348348  match n with
    349349  | One ->
     
    355355    (match m with
    356356     | One -> Bool.False
    357      | P1 q -> eqb0 p q
     357     | P1 q -> eqb p q
    358358     | P0 x -> Bool.False)
    359359  | P0 p ->
     
    361361     | One -> Bool.False
    362362     | P1 x -> Bool.False
    363      | P0 q -> eqb0 p q)
     363     | P0 q -> eqb p q)
    364364
    365365(** val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     
    380380    __ x x0
    381381
    382 (** val leb0 : pos -> pos -> Bool.bool **)
    383 let rec leb0 n m =
     382(** val leb : pos -> pos -> Bool.bool **)
     383let rec leb n m =
    384384  match partial_minus n m with
    385385  | MinusNeg -> Bool.True
     
    403403  two_power_nat (nat_of_pos p)
    404404
    405 (** val max0 : pos -> pos -> pos **)
    406 let max0 n m =
    407   match leb0 n m with
     405(** val max : pos -> pos -> pos **)
     406let max n m =
     407  match leb n m with
    408408  | Bool.True -> m
    409409  | Bool.False -> n
Note: See TracChangeset for help on using the changeset viewer.