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

    r2601 r2773  
    1717open Nat
    1818
     19open Jmeq
     20
     21open Russell
     22
     23open List
     24
     25open Setoids
     26
     27open Monad
     28
     29open Option
     30
     31(** val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option **)
     32let rec nat_bound_opt n n0 =
     33  match n with
     34  | Nat.O -> Types.None
     35  | Nat.S n' ->
     36    (match n0 with
     37     | Nat.O -> Obj.magic (Monad.m_return0 (Monad.max_def Option.option) __)
     38     | Nat.S n'0 ->
     39       Obj.magic
     40         (Monad.m_bind0 (Monad.max_def Option.option)
     41           (Obj.magic (nat_bound_opt n' n'0)) (fun _ ->
     42           Monad.m_return0 (Monad.max_def Option.option) __)))
     43
    1944type nat_compared =
    2045| Nat_lt of Nat.nat * Nat.nat
     
    2550    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    2651    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
    27 let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_723 x_722 = function
     52let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_1684 x_1683 = function
    2853| Nat_lt (n, m) -> h_nat_lt n m
    2954| Nat_eq n -> h_nat_eq n
     
    3358    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    3459    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
    35 let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_729 x_728 = function
     60let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_1690 x_1689 = function
    3661| Nat_lt (n, m) -> h_nat_lt n m
    3762| Nat_eq n -> h_nat_eq n
     
    4166    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    4267    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
    43 let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_735 x_734 = function
     68let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_1696 x_1695 = function
    4469| Nat_lt (n, m) -> h_nat_lt n m
    4570| Nat_eq n -> h_nat_eq n
     
    4974    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    5075    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
    51 let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_741 x_740 = function
     76let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_1702 x_1701 = function
    5277| Nat_lt (n, m) -> h_nat_lt n m
    5378| Nat_eq n -> h_nat_eq n
     
    5782    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    5883    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
    59 let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_747 x_746 = function
     84let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_1708 x_1707 = function
    6085| Nat_lt (n, m) -> h_nat_lt n m
    6186| Nat_eq n -> h_nat_eq n
     
    6590    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
    6691    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
    67 let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_753 x_752 = function
     92let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_1714 x_1713 = function
    6893| Nat_lt (n, m) -> h_nat_lt n m
    6994| Nat_eq n -> h_nat_eq n
     
    7297(** val nat_compared_inv_rect_Type4 :
    7398    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    74     'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
    75     -> 'a1) -> 'a1 **)
     99    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
     100    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    76101let nat_compared_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
    77   let hcut = nat_compared_rect_Type4 h1 h2 h3 x1 x2 hterm in hcut __ __
     102  let hcut = nat_compared_rect_Type4 h1 h2 h3 x1 x2 hterm in hcut __ __ __
    78103
    79104(** val nat_compared_inv_rect_Type3 :
    80105    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    81     'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
    82     -> 'a1) -> 'a1 **)
     106    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
     107    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    83108let nat_compared_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
    84   let hcut = nat_compared_rect_Type3 h1 h2 h3 x1 x2 hterm in hcut __ __
     109  let hcut = nat_compared_rect_Type3 h1 h2 h3 x1 x2 hterm in hcut __ __ __
    85110
    86111(** val nat_compared_inv_rect_Type2 :
    87112    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    88     'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
    89     -> 'a1) -> 'a1 **)
     113    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
     114    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    90115let nat_compared_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
    91   let hcut = nat_compared_rect_Type2 h1 h2 h3 x1 x2 hterm in hcut __ __
     116  let hcut = nat_compared_rect_Type2 h1 h2 h3 x1 x2 hterm in hcut __ __ __
    92117
    93118(** val nat_compared_inv_rect_Type1 :
    94119    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    95     'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
    96     -> 'a1) -> 'a1 **)
     120    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
     121    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    97122let nat_compared_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
    98   let hcut = nat_compared_rect_Type1 h1 h2 h3 x1 x2 hterm in hcut __ __
     123  let hcut = nat_compared_rect_Type1 h1 h2 h3 x1 x2 hterm in hcut __ __ __
    99124
    100125(** val nat_compared_inv_rect_Type0 :
    101126    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    102     'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __
    103     -> 'a1) -> 'a1 **)
     127    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
     128    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    104129let nat_compared_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
    105   let hcut = nat_compared_rect_Type0 h1 h2 h3 x1 x2 hterm in hcut __ __
     130  let hcut = nat_compared_rect_Type0 h1 h2 h3 x1 x2 hterm in hcut __ __ __
    106131
    107132(** val nat_compared_discr :
    108133    Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
    109134let nat_compared_discr a1 a2 x y =
     135  Logic.eq_rect_Type2 x
     136    (match x with
     137     | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
     138     | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
     139     | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
     140
     141(** val nat_compared_jmdiscr :
     142    Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
     143let nat_compared_jmdiscr a1 a2 x y =
    110144  Logic.eq_rect_Type2 x
    111145    (match x with
Note: See TracChangeset for help on using the changeset viewer.