Changeset 2773 for extracted/extranat.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/extranat.ml
r2601 r2773 17 17 open Nat 18 18 19 open Jmeq 20 21 open Russell 22 23 open List 24 25 open Setoids 26 27 open Monad 28 29 open Option 30 31 (** val nat_bound_opt : Nat.nat > Nat.nat > __ Types.option **) 32 let 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 19 44 type nat_compared = 20 45  Nat_lt of Nat.nat * Nat.nat … … 25 50 (Nat.nat > Nat.nat > 'a1) > (Nat.nat > 'a1) > (Nat.nat > Nat.nat > 26 51 '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= function52 let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_1684 x_1683 = function 28 53  Nat_lt (n, m) > h_nat_lt n m 29 54  Nat_eq n > h_nat_eq n … … 33 58 (Nat.nat > Nat.nat > 'a1) > (Nat.nat > 'a1) > (Nat.nat > Nat.nat > 34 59 '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= function60 let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_1690 x_1689 = function 36 61  Nat_lt (n, m) > h_nat_lt n m 37 62  Nat_eq n > h_nat_eq n … … 41 66 (Nat.nat > Nat.nat > 'a1) > (Nat.nat > 'a1) > (Nat.nat > Nat.nat > 42 67 '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= function68 let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_1696 x_1695 = function 44 69  Nat_lt (n, m) > h_nat_lt n m 45 70  Nat_eq n > h_nat_eq n … … 49 74 (Nat.nat > Nat.nat > 'a1) > (Nat.nat > 'a1) > (Nat.nat > Nat.nat > 50 75 '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= function76 let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_1702 x_1701 = function 52 77  Nat_lt (n, m) > h_nat_lt n m 53 78  Nat_eq n > h_nat_eq n … … 57 82 (Nat.nat > Nat.nat > 'a1) > (Nat.nat > 'a1) > (Nat.nat > Nat.nat > 58 83 '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= function84 let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_1708 x_1707 = function 60 85  Nat_lt (n, m) > h_nat_lt n m 61 86  Nat_eq n > h_nat_eq n … … 65 90 (Nat.nat > Nat.nat > 'a1) > (Nat.nat > 'a1) > (Nat.nat > Nat.nat > 66 91 '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= function92 let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_1714 x_1713 = function 68 93  Nat_lt (n, m) > h_nat_lt n m 69 94  Nat_eq n > h_nat_eq n … … 72 97 (** val nat_compared_inv_rect_Type4 : 73 98 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 **) 76 101 let 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 __ __ __ 78 103 79 104 (** val nat_compared_inv_rect_Type3 : 80 105 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 **) 83 108 let 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 __ __ __ 85 110 86 111 (** val nat_compared_inv_rect_Type2 : 87 112 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 **) 90 115 let 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 __ __ __ 92 117 93 118 (** val nat_compared_inv_rect_Type1 : 94 119 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 **) 97 122 let 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 __ __ __ 99 124 100 125 (** val nat_compared_inv_rect_Type0 : 101 126 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 **) 104 129 let 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 __ __ __ 106 131 107 132 (** val nat_compared_discr : 108 133 Nat.nat > Nat.nat > nat_compared > nat_compared > __ **) 109 134 let 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 > __ **) 143 let nat_compared_jmdiscr a1 a2 x y = 110 144 Logic.eq_rect_Type2 x 111 145 (match x with
Note: See TracChangeset
for help on using the changeset viewer.