31 (** val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option **)
32 let rec nat_bound_opt n n0 =
37 | Nat.O -> Obj.magic (Monad.m_return0 (Monad.max_def Option.option) __)
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) __)))
45 | Nat_lt of Nat.nat * Nat.nat
47 | Nat_gt of Nat.nat * Nat.nat
49 (** val nat_compared_rect_Type4 :
50 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
51 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
52 let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_1125 x_1124 = function
53 | Nat_lt (n, m) -> h_nat_lt n m
54 | Nat_eq n -> h_nat_eq n
55 | Nat_gt (n, m) -> h_nat_gt n m
57 (** val nat_compared_rect_Type5 :
58 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
59 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
60 let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_1131 x_1130 = function
61 | Nat_lt (n, m) -> h_nat_lt n m
62 | Nat_eq n -> h_nat_eq n
63 | Nat_gt (n, m) -> h_nat_gt n m
65 (** val nat_compared_rect_Type3 :
66 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
67 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
68 let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_1137 x_1136 = function
69 | Nat_lt (n, m) -> h_nat_lt n m
70 | Nat_eq n -> h_nat_eq n
71 | Nat_gt (n, m) -> h_nat_gt n m
73 (** val nat_compared_rect_Type2 :
74 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
75 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
76 let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_1143 x_1142 = function
77 | Nat_lt (n, m) -> h_nat_lt n m
78 | Nat_eq n -> h_nat_eq n
79 | Nat_gt (n, m) -> h_nat_gt n m
81 (** val nat_compared_rect_Type1 :
82 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
83 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
84 let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_1149 x_1148 = function
85 | Nat_lt (n, m) -> h_nat_lt n m
86 | Nat_eq n -> h_nat_eq n
87 | Nat_gt (n, m) -> h_nat_gt n m
89 (** val nat_compared_rect_Type0 :
90 (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
91 'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
92 let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_1155 x_1154 = function
93 | Nat_lt (n, m) -> h_nat_lt n m
94 | Nat_eq n -> h_nat_eq n
95 | Nat_gt (n, m) -> h_nat_gt n m
97 (** val nat_compared_inv_rect_Type4 :
98 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
99 __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
100 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
101 let nat_compared_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
102 let hcut = nat_compared_rect_Type4 h1 h2 h3 x1 x2 hterm in hcut __ __ __
104 (** val nat_compared_inv_rect_Type3 :
105 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
106 __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
107 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
108 let nat_compared_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
109 let hcut = nat_compared_rect_Type3 h1 h2 h3 x1 x2 hterm in hcut __ __ __
111 (** val nat_compared_inv_rect_Type2 :
112 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
113 __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
114 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
115 let nat_compared_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
116 let hcut = nat_compared_rect_Type2 h1 h2 h3 x1 x2 hterm in hcut __ __ __
118 (** val nat_compared_inv_rect_Type1 :
119 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
120 __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
121 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
122 let nat_compared_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
123 let hcut = nat_compared_rect_Type1 h1 h2 h3 x1 x2 hterm in hcut __ __ __
125 (** val nat_compared_inv_rect_Type0 :
126 Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
127 __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
128 -> __ -> __ -> __ -> 'a1) -> 'a1 **)
129 let nat_compared_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
130 let hcut = nat_compared_rect_Type0 h1 h2 h3 x1 x2 hterm in hcut __ __ __
132 (** val nat_compared_discr :
133 Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
134 let nat_compared_discr a1 a2 x y =
135 Logic.eq_rect_Type2 x
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
141 (** val nat_compared_jmdiscr :
142 Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
143 let nat_compared_jmdiscr a1 a2 x y =
144 Logic.eq_rect_Type2 x
146 | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
147 | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
148 | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
150 (** val nat_compare : Nat.nat -> Nat.nat -> nat_compared **)
151 let rec nat_compare n m =
155 | Nat.O -> Nat_eq Nat.O
156 | Nat.S m' -> Nat_lt (Nat.O, m'))
159 | Nat.O -> Nat_gt (n', Nat.O)
161 (match nat_compare n' m' with
162 | Nat_lt (x, y) -> Nat_lt ((Nat.S x), y)
163 | Nat_eq x -> Nat_eq (Nat.S x)
164 | Nat_gt (x, y) -> Nat_gt (x, (Nat.S y))))
166 (** val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum **)
167 let rec eq_nat_dec n m =
171 | Nat.O -> Types.Inl __
172 | Nat.S m' -> Types.Inr __)
175 | Nat.O -> Types.Inr __
177 (match eq_nat_dec n' m' with
178 | Types.Inl _ -> Types.Inl __
179 | Types.Inr _ -> Types.Inr __))