3 module Snapshot_flyspeck_build_2010_02_12 = struct
4 (* contains hypermap types, so must be loaded late in the build *)
5 let hol_version = "2.20++";;
6 let hol_snapshot = "7_31_09";;
7 let svn_version = 1524;; (* I think, I didn't make a careful record. Definitely pre-1525. *)
8 let the_filetable = [("general/flyspeck_utility.hl", 832);
9 ("general/update_database_310.ml", 832); ("hypermap/hypermap.hl", 832);
10 ("volume/vol1.hl", 737); ("trigonometry/trigonometry.hl", 719);
11 ("general/flyspeck_utility.hl", 717); ("trigonometry/trig2.hl", 717);
12 ("trigonometry/trig1.hl", 708); ("nonlinear/ineqdata3q1h.hl", 707);
13 ("nonlinear/ineq.hl", 707); ("leg/enclosed_def.hl", 707);
14 ("leg/quadratic_root_plus_def.hl", 706);
15 ("leg/abc_of_quadratic_def.hl", 705); ("leg/muR_def.hl", 704);
16 ("leg/collect_geom.hl", 703); ("leg/cayleyR_def.hl", 678);
17 ("leg/affprops.hl", 677); ("leg/AFF_SGN_TAC.hl", 677);
18 ("leg/geomdetail.hl", 677); ("pervasives", 673)];;
20 [ (* ("geomdetail'simplex", `:(real^3->bool)->(real^3->bool)->bool`); *)
21 ("map3", `:real^3->real^3->real^3`);
22 ("canon", `:(A)hypermap->((A)loop->bool)->((A->bool)->bool)->bool`);
23 ("is_flag", `:(A)hypermap->((A->bool)->bool)->bool`);
24 ("is_gen_flag", `:(A)hypermap->(A->bool)->((A->bool)->bool)->bool`);
25 ("edge_nondegenerate", `:(A)hypermap->bool`);
26 ("face_collection", `:(A)hypermap->(A)loop->bool`);
27 ("face_loop", `:(A)hypermap->A->(A)loop`);
28 ("res", `:(A->A)->(A->bool)->A->A`);
29 ("team", `:(A)hypermap->(A)loop->(A->bool)->bool`);
30 ("iso", `:(A)hypermap->(B)hypermap->bool`);
31 ("quotient", `:(A)hypermap->((A)loop->bool)->(A->bool)hypermap`);
32 ("nmap", `:(A)hypermap->((A)loop->bool)->(A->bool)->A->bool`);
33 ("fmap", `:(A)hypermap->((A)loop->bool)->(A->bool)->A->bool`);
34 ("tail", `:(A)hypermap->((A)loop->bool)->A->A`);
35 ("head", `:(A)hypermap->((A)loop->bool)->A->A`);
36 ("choice", `:(A)hypermap->((A)loop->bool)->A->A->bool`);
37 ("support_darts", `:((A)loop->bool)->A->bool`);
38 ("quotient_darts", `:(A)hypermap->((A)loop->bool)->(A->bool)->bool`);
39 ("is_normal", `:(A)hypermap->((A)loop->bool)->bool`);
40 ("atom", `:(A)hypermap->(A)loop->A->A->bool`);
41 ("is_node_going", `:(A)hypermap->(A)loop->A->A->bool`);
42 ("in_path", `:(num->A)->num->A->bool`);
43 ("set_dart_of", `:(num->A)->num->A->bool`);
44 ("contour_of", `:(A)loop->A->num->A`);
45 ("is_loop", `:(A)hypermap->(A)loop->bool`); ("top", `:(A)loop->num`);
46 ("size", `:(A)loop->num`); ("inside", `:A->(A)loop->bool`);
47 ("back", `:(A)loop->A->A`); ("next", `:(A)loop->A->A`);
48 ("dart_of", `:(A)loop->A->bool`);
49 ("tuple_loop", `:(A)loop->(A->bool)#(A->A)`);
50 ("loop", `:(A->bool)#(A->A)->(A)loop`);
51 ("shift_path", `:(num->A)->num->num->A`);
52 ("is_Moebius_contour", `:(A)hypermap->(num->A)->num->bool`);
53 ("is_splitting_component", `:(A)hypermap->A->bool`);
54 ("planar_ind", `:(A)hypermap->real`);
55 ("is_face_split", `:(A)hypermap->A->bool`);
56 ("is_node_split", `:(A)hypermap->A->bool`);
57 ("is_edge_split", `:(A)hypermap->A->bool`);
58 ("is_face_merge", `:(A)hypermap->A->bool`);
59 ("is_node_merge", `:(A)hypermap->A->bool`);
60 ("is_edge_merge", `:(A)hypermap->A->bool`);
61 ("inj_orbit", `:(A->A)->A->num->bool`);
62 ("double_face_walkup", `:(A)hypermap->A->A->(A)hypermap`);
63 ("double_node_walkup", `:(A)hypermap->A->A->(A)hypermap`);
64 ("double_edge_walkup", `:(A)hypermap->A->A->(A)hypermap`);
65 ("face_walkup", `:(A)hypermap->A->(A)hypermap`);
66 ("node_walkup", `:(A)hypermap->A->(A)hypermap`);
67 ("edge_walkup", `:(A)hypermap->A->(A)hypermap`);
68 ("shift", `:(A)hypermap->(A)hypermap`);
69 ("is_face_degenerate", `:(A)hypermap->A->bool`);
70 ("is_node_degenerate", `:(A)hypermap->A->bool`);
71 ("is_edge_degenerate", `:(A)hypermap->A->bool`);
72 ("isolated_dart", `:(A)hypermap->A->bool`);
73 ("is_inj_contour", `:(A)hypermap->(num->A)->num->bool`);
74 ("face_contour", `:(A)hypermap->A->num->A`);
75 ("node_contour", `:(A)hypermap->A->num->A`);
76 ("is_contour", `:(A)hypermap->(num->A)->num->bool`);
77 ("one_step_contour", `:(A)hypermap->A->A->bool`);
78 ("face_path", `:(A)hypermap->A->num->A`);
79 ("node_path", `:(A)hypermap->A->num->A`);
80 ("edge_path", `:(A)hypermap->A->num->A`);
81 ("connected_hypermap", `:(A)hypermap->bool`);
82 ("dart_nondegenerate", `:(A)hypermap->A->bool`);
83 ("dart_degenerate", `:(A)hypermap->A->bool`);
84 ("simple_hypermap", `:(A)hypermap->bool`);
85 ("planar_hypermap", `:(A)hypermap->bool`);
86 ("plain_hypermap", `:(A)hypermap->bool`);
87 ("number_of_components", `:(A)hypermap->num`);
88 ("number_of_faces", `:(A)hypermap->num`);
89 ("number_of_nodes", `:(A)hypermap->num`);
90 ("number_of_edges", `:(A)hypermap->num`);
91 ("set_of_components", `:(A)hypermap->(A->bool)->bool`);
92 ("set_part_components", `:(A)hypermap->(A->bool)->(A->bool)->bool`);
93 ("set_components", `:(A)hypermap->(A->bool)->(A->bool)->bool`);
94 ("face_set", `:(A)hypermap->(A->bool)->bool`);
95 ("node_set", `:(A)hypermap->(A->bool)->bool`);
96 ("edge_set", `:(A)hypermap->(A->bool)->bool`);
97 ("number_of_orbits", `:(A->bool)->(A->A)->num`);
98 ("set_of_orbits", `:(A->bool)->(A->A)->(A->bool)->bool`);
99 ("comb_component", `:(A)hypermap->A->A->bool`);
100 ("is_in_component", `:(A)hypermap->A->A->bool`);
101 ("is_path", `:(A)hypermap->(num->A)->num->bool`);
102 ("go_one_step", `:(A)hypermap->A->A->bool`);
103 ("face", `:(A)hypermap->A->A->bool`);
104 ("node", `:(A)hypermap->A->A->bool`);
105 ("edge", `:(A)hypermap->A->A->bool`); ("face_map", `:(A)hypermap->A->A`);
106 ("node_map", `:(A)hypermap->A->A`); ("edge_map", `:(A)hypermap->A->A`);
107 ("dart", `:(A)hypermap->A->bool`);
108 ("tuple_hypermap", `:(A)hypermap->(A->bool)#(A->A)#(A->A)#(A->A)`);
109 ("hypermap", `:(A->bool)#(A->A)#(A->A)#(A->A)->(A)hypermap`);
110 ("orbit_map", `:(A->A)->A->A->bool`); ("POWER", `:(A->A)->num->A->A`);
111 ("integer_point", `:(real^3->bool)->real^3->bool`);
112 ("map1", `:real^3->real^3->bool`);
113 ("close_hinhcau", `:real^3->real->real^3->bool`);
114 ("set_of_ccube", `:(real^3->bool)->(real^3->bool)->bool`);
115 ("ccube", `:real^3->real^3->bool`);
116 ("vector_to_pair", `:real^3->real#real#real`);
117 ("int_interval", `:real->real->real->bool`);
118 ("map0", `:real^3->real^3->bool`);
119 ("union_of_int_cube", `:real^3->real->real^3->bool`);
120 ("int_ball", `:real^3->real->real^3->bool`);
121 ("union_of_cube", `:real^3->real->real^3->bool`);
122 ("set_of_cube", `:(real^3->bool)->(real^3->bool)->bool`);
123 ("hinhcau", `:real^3->real->real^3->bool`);
124 ("cube", `:real^3->real^3->bool`);
125 ("sol", `:(real^3->bool)->real^3->real`);
126 ("volume_prop_fix", `:((real^3->bool)->real)->bool`);
127 ("eventually_radial_norm", `:real^A->(real^A->bool)->bool`);
128 ("radial_norm", `:real->real^A->(real^A->bool)->bool`);
129 ("parallel", `:real^N->real^N->bool`); ("unknown", `:bool`);
130 ("arg_diff", `:real^2->real^2->real`); ("pl_angle", `:real^2->real`);
131 ("polar_cycle_on", `:(real^2->real^2)->(real^2->bool)->bool`);
132 ("polar_le", `:real^2->real^2->bool`);
133 ("polar_lt", `:real^2->real^2->bool`); ("tri_itv", `:real->bool`);
134 ("real_itv", `:real->real->real->bool`);
135 ("sinV", `:real^A->real^A->real`); ("cosV", `:real^A->real^A->real`);
136 ("atan2_temp", `:real#real->real`);
138 `:real->real->real->real->real->real->real->real->real->real`);
139 ("quadratic_root_plus", `:real#real#real->real`);
140 ("abc_of_quadratic", `:(real->real)->real#real#real`);
142 `:real->real->real->real->real->real->real->real->real->real->real`);
143 ("muy_v", `:real^N->real^N->real^N->real^N->real^N->real->real`);
144 ("muy_delta", `:real->real->real->real->real->real->real`);
145 ("det_vec3", `:real^3->real^3->real^3->real`);
147 `:real^3->real^3->real^3->real^3->real->real->real->real->real->A->bool`);
148 ("coplanar_alt", `:(real^A->bool)->bool`);
150 `:real->real->real->real->real->real->real->real->real->real->real`);
151 ("delta_x14", `:real->real->real->real->real->real->real`);
152 ("delta_x13", `:real->real->real->real->real->real->real`);
153 ("delta_x12", `:real->real->real->real->real->real->real`);
154 ("coef3", `:real^N->real^N->real^N->real^N->real`);
155 ("coef2", `:real^N->real^N->real^N->real^N->real`);
156 ("coef1", `:real^N->real^N->real^N->real^N->real`);
157 ("c_coef", `:real->real->real->real->real->real`);
158 ("b_coef", `:real->real->real->real->real->real`);
159 ("cm3_ups_x", `:real^3->real^3->real^3->real`);
160 ("plane_3p", `:real^3->real^3->real^3->real^3->bool`);
161 ("delta_x34", `:real->real->real->real->real->real->real`);
162 ("plane_norm", `:(real^A->bool)->bool`);
163 ("ups_x_pow2", `:real->real->real->real`);
164 ("max_real3", `:real->real->real->real`);
165 ("max_real", `:real->real->real`);
166 ("eta_v", `:real^N->real^N->real^N->real`);
167 ("delta", `:real->real->real->real->real->real->real`);
168 ("chi", `:real->real->real->real->real->real->real`);
169 ("rho_ij", `:real->real->real->real->real->real->real`);
171 `:real->real->real->real->real->real->real->real->real->real->real`);
172 ("min_dist", `:real^3->(real^3->bool)->bool`);
173 ("e_plane", `:real^N->real^N->real^N->bool`);
174 ("near2t0", `:real^A->(real^A->bool)->real^A->bool`);
175 ("near", `:real^N->real->(real^N->bool)->real^N->bool`);
176 ("VC_INFI", `:(real^3->bool)->real^3->bool`);
177 ("VC", `:real^3->(real^3->bool)->real^3->bool`);
178 ("lambda_y", `:real^3->(real^3->bool)->real^3->bool`);
179 ("lambda_x", `:real^3->(real^3->bool)->real^3->bool`);
180 ("VC_INFI_trg", `:(real^3->bool)->real^3->bool`);
181 ("VC_trg", `:real^3->(real^3->bool)->real^3->bool`);
182 ("unobstructed", `:real^3->real^3->(real^3->bool)->bool`);
183 ("obstruct", `:real^3->real^3->(real^3->bool)->bool`);
184 ("conv", `:(real^A->bool)->real^A->bool`);
185 ("obstructed", `:real^3->real^3->(real^3->bool)->bool`);
186 ("barrier", `:(real^3->bool)->(real^3->bool)->bool`);
187 ("Q_SYS", `:(real^3->bool)->(real^3->bool)->bool`);
188 ("anchor_points", `:real^3->real^3->(real^3->bool)->real^3->bool`);
189 ("anchor", `:real^3->real^3->real^3->(real^3->bool)->bool`);
190 ("isolated_pai", `:(real^3->bool)->(real^3->bool)->(real^3->bool)->bool`);
191 ("isolated_qua", `:(real^3->bool)->(real^3->bool)->bool`);
193 `:real^3->real^3->real^3->real^3->real^3->(real^3->bool)->bool`);
195 `:real^3->real^3->real^3->real^3->real^3->(real^3->bool)->bool`);
197 `:real^3->real^3->real^3->real^3->real^3->(real^3->bool)->bool`);
199 `:real^3->real^3->real^3->real^3->real^3->real^3->(real^3->bool)->bool`);
200 ("strict_qua2", `:(real^3->bool)->(real^3->bool)->(real^3->bool)->bool`);
201 ("strict_qua", `:(real^3->bool)->(real^3->bool)->bool`);
202 ("diagonal", `:real^3->real^3->(real^3->bool)->(real^3->bool)->bool`);
203 ("quarter", `:(real^3->bool)->(real^3->bool)->bool`);
204 ("quasi_reg_tet", `:(real^3->bool)->(real^3->bool)->bool`);
205 ("simplex", `:(real^3->bool)->(real^3->bool)->bool`);
206 ("quasi_tri", `:(real^3->bool)->(real^3->bool)->bool`); ("t0", `:real`);
207 ("voro2", `:real^3->(real^3->bool)->real^3->bool`);
208 ("voronoi2", `:real^3->(real^3->bool)->real^3->bool`);
209 ("d3", `:real^3->real^3->real`);
210 ("centered_pac", `:(real^3->bool)->real^3->bool`);
211 ("center_pac", `:(real^3->bool)->real^3->bool`);
212 ("packing_trg", `:(real^3->bool)->bool`);
213 ("border", `:(real^A->bool)->real^A->bool`);
214 ("conv_trg", `:(real^A->bool)->real^A->bool`);
215 ("conv0_2", `:(real^A->bool)->real^A->bool`);
216 ("voronoi_trg", `:real^A->(real^A->bool)->real^A->bool`);
217 ("ineq", `:(real#real#real)list->bool->bool`);
218 ("abc_param", `:real^A->real^A->real^A->B->real#real#B`);
220 `:real^3->real^3->real^3->real^3->real->real->real->real^3`);
221 ("ortho0", `:real^A->real^A->real^A->real^A->real^A->bool`);
222 ("rcone_lt", `:real^A->real^A->real->real^A->bool`);
223 ("eventually_radial", `:real^A->(real^A->bool)->bool`);
224 ("radial", `:real->real^A->(real^A->bool)->bool`);
225 ("null_equiv", `:(real^3->bool)#(real^3->bool)->bool`);
226 ("packing", `:(real^3->bool)->bool`);
227 ("azim_cycle", `:(real^3->bool)->real^3->real^3->real^3->real^3`);
228 ("projection", `:real^A->real^A->real^A`);
229 ("cyclic_set", `:(real^A->bool)->real^A->real^A->bool`);
230 ("polar_cycle", `:(real#real->bool)->real#real->real#real`);
231 ("cyclic_order", `:real#real->real#real->real#real->bool`);
232 ("radius", `:real#real->real`);
233 ("directed_angle", `:real#real->real#real->real`);
234 ("beta", `:real->real->real`);
235 ("euler_p", `:real^A->real^A->real^A->real^A->real`);
237 `:real^A->real^A->real^A->real^A->real#real#real#real#real#real`);
239 `:real^A->real^A->real^A->real^A->real#real#real#real#real#real`);
240 ("orientation", `:(real^A->bool)->real^A->(real->bool)->bool`);
241 ("radV", `:(real^A->bool)->real`);
242 ("circumcenter", `:(real^A->bool)->real^A`);
243 ("bis_lt", `:real^A->real^A->real^A->bool`);
244 ("bis_le", `:real^A->real^A->real^A->bool`);
245 ("bis", `:real^A->real^A->real^A->bool`);
246 ("open_half_space", `:(real^A->bool)->bool`);
247 ("closed_half_space", `:(real^A->bool)->bool`);
248 ("open_half_plane", `:(real^A->bool)->bool`);
249 ("closed_half_plane", `:(real^A->bool)->bool`);
250 ("line", `:(real^A->bool)->bool`);
251 ("voronoi_le", `:real^A->(real^A->bool)->real^A->bool`);
252 ("voronoi", `:real^A->(real^A->bool)->real^A->bool`);
253 ("aff", `:(real^A->bool)->real^A->bool`);
254 ("rad2_x", `:real->real->real->real->real->real->real`);
255 ("dihR", `:real->real->real->real`); ("solR", `:real->real->real->real`);
256 ("volR", `:real->real->real->real`);
257 ("arclength", `:real->real->real->real`);
258 ("vol_x", `:real->real->real->real->real->real->real`);
259 ("tauq", `:real->real->real->real->real->real->real->real->real->real`);
260 ("taum", `:real->real->real->real->real->real->real`);
261 ("lnazim", `:real->real->real->real->real->real->real`);
262 ("rhazim", `:real->real->real->real->real->real->real`);
263 ("rho", `:real->real`); ("ly", `:real->real`); ("const1", `:real`);
264 ("interp", `:real->real->real->real->real->real`);
265 ("sol_y", `:real->real->real->real->real->real->real`);
266 ("sol_x", `:real->real->real->real->real->real->real`);
267 ("dih3_x", `:real->real->real->real->real->real->real`);
268 ("dih2_x", `:real->real->real->real->real->real->real`);
269 ("dih3_y", `:real->real->real->real->real->real->real`);
270 ("dih2_y", `:real->real->real->real->real->real->real`);
271 ("dih_y", `:real->real->real->real->real->real->real`);
272 ("dih_x", `:real->real->real->real->real->real->real`);
273 ("chi_x", `:real->real->real->real->real->real->real`);
274 ("rho_x", `:real->real->real->real->real->real->real`);
275 ("eta_y", `:real->real->real->real`);
276 ("eta_x", `:real->real->real->real`);
277 ("ups_x", `:real->real->real->real`);
278 ("delta_x6", `:real->real->real->real->real->real->real`);
279 ("delta_x4", `:real->real->real->real->real->real->real`);
280 ("delta_y", `:real->real->real->real->real->real->real`);
281 ("pi_rt18", `:real`); ("sqrt2", `:real`); ("sqrt8", `:real`);
282 ("atn2", `:real#real->real`); ("SDIFF", `:(A->bool)->(A->bool)->A->bool`);
283 ("vol_ball_wedge", `:real^3->real^3->real^3->real^3->real->real`);
284 ("vol_rect", `:real^A->real^B->real`);
285 ("vol_conv", `:real^A->real^A->real^A->real^A->real`);
286 ("vol_conic_cap_wedge",
287 `:real^3->real^3->real^3->real^3->real->real->real`);
288 ("vol_frustt_wedge", `:real^3->real^3->real^3->real^3->real->real->real`);
289 ("vol_solid_triangle", `:real^A->real^A->real^A->real^A->real->real`);
290 ("primitive", `:(real^3->bool)->bool`);
291 ("circular_cone", `:(real^3->bool)->bool`);
292 ("c_cone", `:real^3#real^3#real->real^3->bool`);
293 ("sphere", `:(real^3->bool)->bool`);
294 ("rect", `:real^3->real^3->real^3->bool`);
295 ("solid_triangle", `:real^A->(real^A->bool)->real->real^A->bool`);
296 ("cone0", `:real^A->(real^A->bool)->real^A->bool`);
297 ("cone", `:real^A->(real^A->bool)->real^A->bool`);
298 ("dihV", `:real^A->real^A->real^A->real^A->real`);
299 ("opposite", `:real^N->real^N->(real^N->bool)->bool`);
300 ("wedge", `:real^3->real^3->real^3->real^3->real^3->bool`);
301 ("azim", `:real^3->real^3->real^3->real^3->real`);
302 ("arcV", `:real^A->real^A->real^A->real`);
303 ("orthonormal", `:real^3->real^3->real^3->bool`);
304 ("conic_cap", `:real^A->real^A->real->real->real^A->bool`);
305 ("ellipsoid", `:real^3->real->real^3->bool`);
306 ("normball", `:real^A->real->real^A->bool`);
307 ("scale", `:real^3->real^3->real^3`);
308 ("frustt", `:real^A->real^A->real->real->real^A->bool`);
309 ("frustum", `:real^N->real^N->real->real->real->real^N->bool`);
310 ("rcone_eq", `:real^A->real^A->real->real^A->bool`);
311 ("rcone_ge", `:real^A->real^A->real->real^A->bool`);
312 ("rcone_gt", `:real^A->real^A->real->real^A->bool`);
313 ("rconesgn", `:(real->real->bool)->real^A->real^A->real->real^A->bool`);
314 ("delta_x", `:real->real->real->real->real->real->real`);
315 ("conv0", `:(real^A->bool)->real^A->bool`);
316 ("aff_le", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
317 ("aff_lt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
318 ("aff_ge", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
319 ("aff_gt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
320 ("sgn_le", `:real->bool`); ("sgn_lt", `:real->bool`);
321 ("sgn_ge", `:real->bool`); ("sgn_gt", `:real->bool`);
322 ("affsign", `:(real->bool)->(real^A->bool)->(real^A->bool)->real^A->bool`);
323 ("lin_combo", `:(real^N->bool)->(real^N->real)->real^N`);
324 ("pad2d3d", `:real^2->real^3`); ("plane", `:(real^A->bool)->bool`);
325 ("slice", `:num->real->(real^A->bool)->real^B->bool`);
326 ("pushin", `:num->B->B^A->B^C`); ("dropout", `:num->real^N->real^M`);
327 ("real_measure", `:(real->bool)->real`);
328 ("real_measurable", `:(real->bool)->bool`);
329 ("has_real_measure", `:(real->bool)->real->bool`);
330 ("absolutely_real_integrable_on", `:(real->real)->(real->bool)->bool`);
331 ("real_negligible", `:(real->bool)->bool`);
332 ("real_integral", `:(real->bool)->(real->real)->real`);
333 ("real_integrable_on", `:(real->real)->(real->bool)->bool`);
334 ("has_real_integral", `:(real->real)->real->(real->bool)->bool`);
335 ("closed_real_interval", `:(real#real)list->real->bool`);
336 ("open_real_interval", `:real#real->real->bool`);
337 ("is_realinterval", `:(real->bool)->bool`);
338 ("real_differentiable_on", `:(real->real)->(real->bool)->bool`);
339 ("higher_real_derivative", `:num->(real->real)->real->real`);
340 ("real_derivative", `:(real->real)->real->real`);
341 ("real_differentiable", `:(real->real)->(real)net->bool`);
342 ("has_real_derivative", `:(real->real)->real->(real)net->bool`);
343 ("real_continuous_on", `:(real->real)->(real->bool)->bool`);
344 ("real_continuous", `:(A->real)->(A)net->bool`);
345 ("at_neginfinity", `:(real)net`); ("at_posinfinity", `:(real)net`);
346 ("atreal", `:real->(real)net`);
347 ("real_summable", `:(num->bool)->(num->real)->bool`);
348 ("real_infsum", `:(num->bool)->(num->real)->real`);
349 ("real_sums", `:(num->real)->real->(num->bool)->bool`);
350 ("--->", `:(A->real)->real->(A)net->bool`);
351 ("real_compact", `:(real->bool)->bool`);
352 ("real_bounded", `:(real->bool)->bool`);
353 ("euclideanreal", `:(real)topology`);
354 ("real_closed", `:(real->bool)->bool`);
355 ("real_open", `:(real->bool)->bool`);
356 ("measure", `:(real^A->bool)->real`);
357 ("measurable", `:(real^A->bool)->bool`);
358 ("has_measure", `:(real^A->bool)->real->bool`);
359 ("*_c", `:(A->bool)->(B->bool)->A#B->bool`);
360 ("+_c", `:(A->bool)->(B->bool)->A+B->bool`);
361 ("ordinal", `:(A#A->bool)->bool`);
362 ("linseg", `:(A#A->bool)->A->A#A->bool`);
363 ("inseg", `:(A#A->bool)->(A#A->bool)->bool`);
364 ("woset", `:(A#A->bool)->bool`);
365 ("chain", `:(A#A->bool)->(A->bool)->bool`);
366 ("poset", `:(A#A->bool)->bool`); ("fl", `:(A#A->bool)->A->bool`);
367 ("less", `:(A#A->bool)->A#A->bool`);
368 ("angle", `:real^A#real^A#real^A->real`);
369 ("vector_angle", `:real^A->real^A->real`); ("acs", `:real->real`);
370 ("asn", `:real->real`); ("cacs", `:real^2->real^2`);
371 ("casn", `:real^2->real^2`); ("atn", `:real->real`);
372 ("catn", `:real^2->real^2`); ("unwinding", `:real^2->real^2`);
373 ("cpow", `:real^2->real^2->real^2`); ("clog", `:real^2->real^2`);
374 ("tan", `:real->real`); ("ctan", `:real^2->real^2`);
375 ("rotate2d", `:real->real^2->real^2`); ("Arg", `:real^2->real`);
376 ("pi", `:real`); ("log", `:real->real`); ("cos", `:real->real`);
377 ("sin", `:real->real`); ("exp", `:real->real`);
378 ("csin", `:real^2->real^2`); ("ccos", `:real^2->real^2`);
379 ("cexp", `:real^2->real^2`);
380 ("analytic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
381 ("holomorphic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
382 ("higher_complex_derivative", `:num->(real^2->real^2)->real^2->real^2`);
383 ("complex_derivative", `:(real^2->real^2)->real^2->real^2`);
384 ("complex_differentiable", `:(real^2->real^2)->(real^2)net->bool`);
385 ("has_complex_derivative", `:(real^2->real^2)->real^2->(real^2)net->bool`);
386 ("cproduct", `:(A->bool)->(A->real^2)->real^2`);
387 ("real", `:real^2->bool`); ("csqrt", `:real^2->real^2`);
388 ("cnj", `:real^2->real^2`); ("complex_pow", `:real^2->num->real^2`);
389 ("complex_div", `:real^2->real^2->real^2`);
390 ("complex_inv", `:real^2->real^2`);
391 ("complex_mul", `:real^2->real^2->real^2`); ("ii", `:real^2`);
392 ("Cx", `:real->real^2`); ("complex", `:real#real->real^2`);
393 ("Im", `:real^2->real`); ("Re", `:real^2->real`);
394 ("absolutely_integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
395 ("negligible", `:(real^A->bool)->bool`);
396 ("indicator", `:(real^M->bool)->real^M->real^1`);
398 `:(real^N->bool)->((real^N->bool)->bool)->num#real->bool`);
399 ("lifted", `:(A->A->B)->(A)option->(A)option->(B)option`);
400 ("operative", `:(A->A->A)->((real^N->bool)->A)->bool`);
401 ("integral", `:(real^A->bool)->(real^A->real^B)->real^B`);
402 ("integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
403 ("has_integral", `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
404 ("has_integral_compact_interval",
405 `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
406 ("fine", `:(A->B->bool)->(A#(B->bool)->bool)->bool`);
407 ("tagged_division_of",
408 `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
409 ("tagged_partial_division_of",
410 `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
411 ("division_of", `:((real^A->bool)->bool)->(real^A->bool)->bool`);
412 ("gauge", `:(real^A->real^A->bool)->bool`);
413 ("content", `:(real^M->bool)->real`);
414 ("interval_lowerbound", `:(real^M->bool)->real^M`);
415 ("interval_upperbound", `:(real^M->bool)->real^M`);
416 ("vector_derivative", `:(real^1->real^N)->(real^1)net->real^N`);
417 ("has_vector_derivative", `:(real^1->real^A)->real^A->(real^1)net->bool`);
418 ("jacobian", `:(real^A->real^B)->(real^A)net->real^A^B`);
419 ("frechet_derivative", `:(real^A->real^B)->(real^A)net->real^A->real^B`);
420 ("differentiable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
421 ("differentiable", `:(real^B->real^A)->(real^B)net->bool`);
423 `:(real^B->real^A)->(real^B->real^A)->(real^B)net->bool`);
424 ("interval_bij", `:real^N#real^N->real^N#real^N->real^N->real^N`);
425 ("retract_of", `:(real^A->bool)->(real^A->bool)->bool`);
426 ("retraction", `:(real^N->bool)#(real^N->bool)->(real^N->real^N)->bool`);
427 ("reduced", `:((num->num)->num->num)->num->(num->num)->num`);
428 ("ksimplex", `:num->num->((num->num)->bool)->bool`);
429 ("kle", `:num->(num->num)->(num->num)->bool`);
430 ("path_connected", `:(real^A->bool)->bool`);
431 ("path_component", `:(real^A->bool)->real^A->real^A->bool`);
432 ("linepath", `:real^A#real^A->real^1->real^A`);
433 ("shiftpath", `:real^1->(real^1->real^N)->real^1->real^N`);
434 ("arc", `:(real^1->real^N)->bool`);
435 ("simple_path", `:(real^1->real^N)->bool`);
436 ("++", `:(real^1->A)->(real^1->A)->real^1->A`);
437 ("reversepath", `:(real^1->real^N)->real^1->real^N`);
438 ("path_image", `:(real^1->real^N)->real^N->bool`);
439 ("pathfinish", `:(real^1->real^N)->real^N`);
440 ("pathstart", `:(real^1->real^N)->real^N`);
441 ("path", `:(real^1->real^N)->bool`);
442 ("extreme_point_of", `:real^A->(real^A->bool)->bool`);
443 ("face_of", `:(real^A->bool)->(real^A->bool)->bool`);
444 ("relative_interior", `:(real^A->bool)->real^A->bool`);
445 ("starlike", `:(real^A->bool)->bool`);
447 `:(real^N->bool)->(real^N->real)->real^(N,1)finite_sum->bool`);
448 ("convex_on", `:(real^A->real)->(real^A->bool)->bool`);
449 ("coplanar", `:(real^A->bool)->bool`);
450 ("affine_dependent", `:(real^N->bool)->bool`);
451 ("conic", `:(real^A->bool)->bool`); ("convex", `:(real^A->bool)->bool`);
452 ("affine", `:(real^A->bool)->bool`);
453 ("closest_point", `:(real^A->bool)->real^A->real^A`);
454 ("from", `:num->num->bool`);
455 ("summable", `:(num->bool)->(num->real^A)->bool`);
456 ("infsum", `:(num->bool)->(num->real^A)->real^A`);
457 ("sums", `:(num->real^A)->real^A->(num->bool)->bool`);
458 ("homeomorphic", `:(real^A->bool)->(real^B->bool)->bool`);
460 `:(real^B->bool)#(real^A->bool)->(real^B->real^A)#(real^A->real^B)->bool`);
461 ("open_segment", `:real^A#real^A->real^A->bool`);
462 ("closed_segment", `:(real^A#real^A)list->real^A->bool`);
463 ("is_interval", `:(real^N->bool)->bool`);
464 ("closed_interval", `:(real^N#real^N)list->real^N->bool`);
465 ("open_interval", `:real^N#real^N->real^N->bool`);
466 ("diameter", `:(real^A->bool)->real`);
467 ("connected_component", `:(real^A->bool)->real^A->real^A->bool`);
468 ("uniformly_continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
469 ("continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
470 ("continuous", `:(B->real^A)->(B)net->bool`);
471 ("complete", `:(real^N->bool)->bool`); ("cauchy", `:(num->real^N)->bool`);
472 ("compact", `:(real^N->bool)->bool`);
473 ("bounded", `:(real^N->bool)->bool`); ("netlimit", `:(A)net->A`);
474 ("lim", `:(A)net->(A->real^B)->real^B`);
475 ("-->", `:(B->real^A)->real^A->(B)net->bool`);
476 ("eventually", `:(A->bool)->(A)net->bool`);
477 ("trivial_limit", `:(A)net->bool`);
478 ("in_direction", `:real^A->real^A->(real^A)net`);
479 ("within", `:(A)net->(A->bool)->(A)net`); ("sequentially", `:(num)net`);
480 ("at_infinity", `:(real^A)net`); ("at", `:real^A->(real^A)net`);
481 ("netord", `:(A)net->A->A->bool`); ("mk_net", `:(A->A->bool)->(A)net`);
482 ("frontier", `:(real^A->bool)->real^A->bool`);
483 ("closure", `:(real^A->bool)->real^A->bool`);
484 ("interior", `:(real^A->bool)->real^A->bool`);
485 ("limit_point_of", `:real^A->(real^A->bool)->bool`);
486 ("connected", `:(real^A->bool)->bool`);
487 ("cball", `:real^A#real->real^A->bool`);
488 ("ball", `:real^A#real->real^A->bool`);
489 ("euclidean", `:(real^A)topology`); ("closed", `:(real^N->bool)->bool`);
490 ("open", `:(real^A->bool)->bool`);
491 ("subtopology", `:(A)topology->(A->bool)->(A)topology`);
492 ("closed_in", `:(A)topology->(A->bool)->bool`);
493 ("topspace", `:(A)topology->A->bool`);
494 ("open_in", `:(A)topology->(A->bool)->bool`);
495 ("topology", `:((A->bool)->bool)->(A)topology`);
496 ("istopology", `:((A->bool)->bool)->bool`);
497 ("ITER", `:num->(A->A)->A->A`); ("frac", `:real->real`);
498 ("floor", `:real->real`); ("integer", `:real->bool`);
499 ("cross", `:real^3->real^3->real^3`);
500 ("rotoinversion_matrix", `:real^A^A->bool`);
501 ("rotation_matrix", `:real^A^A->bool`);
502 ("orthogonal_matrix", `:real^N^N->bool`);
503 ("orthogonal_transformation", `:(real^N->real^N)->bool`);
504 ("det", `:real^N^N->real`); ("trace", `:real^N^N->real`);
505 ("product", `:(A->bool)->(A->real)->real`); ("sign", `:(A->A)->real`);
506 ("evenperm", `:(A->A)->bool`); ("permutation", `:(A->A)->bool`);
507 ("swapseq", `:num->(A->A)->bool`); ("swap", `:A#A->A->A`);
508 ("inverse", `:(B->A)->A->B`); ("permutes", `:(A->A)->(A->bool)->bool`);
509 ("midpoint", `:real^A#real^A->real^A`);
510 ("between", `:real^A->real^A#real^A->bool`);
511 ("collinear", `:(real^A->bool)->bool`); ("infnorm", `:real^N->real`);
512 ("rank", `:real^M^N->num`); ("columnvector", `:real^N->real^1^N`);
513 ("rowvector", `:real^N->real^N^1`); ("dim", `:(real^A->bool)->num`);
514 ("independent", `:(real^A->bool)->bool`);
515 ("dependent", `:(real^A->bool)->bool`);
516 ("span", `:(real^A->bool)->real^A->bool`);
517 ("subspace", `:(real^A->bool)->bool`); ("drop", `:real^1->real`);
518 ("lift", `:real->real^1`); ("onorm", `:(real^M->real^N)->real`);
519 ("matrix", `:(real^M->real^N)->real^M^N`);
520 ("matrix_inv", `:real^N^M->real^M^N`); ("invertible", `:real^N^M->bool`);
521 ("columns", `:real^N^M->real^M->bool`);
522 ("rows", `:real^N^M->real^N->bool`); ("column", `:num->real^N^M->real^M`);
523 ("row", `:num->real^N^M->real^N`); ("transp", `:real^N^M->real^M^N`);
524 ("mat", `:num->real^N^M`);
525 ("vector_matrix_mul", `:real^M->real^N^M->real^N`);
526 ("matrix_vector_mul", `:real^N^M->real^N->real^M`);
527 ("matrix_mul", `:real^N^M->real^P^N->real^P^M`);
528 ("matrix_sub", `:real^N^M->real^N^M->real^N^M`);
529 ("matrix_add", `:real^N^M->real^N^M->real^N^M`);
530 ("matrix_neg", `:real^N^M->real^N^M`);
531 ("adjoint", `:(real^M->real^N)->real^N->real^M`);
532 ("bilinear", `:(real^A->real^B->real^C)->bool`);
533 ("linear", `:(real^M->real^N)->bool`);
534 ("orthogonal", `:real^A->real^A->bool`); ("basis", `:num->real^A`);
535 ("vsum", `:(A->bool)->(A->real^N)->real^N`);
536 ("distance", `:real^A#real^A->real`); ("vector_norm", `:real^A->real`);
537 ("dot", `:real^N->real^N->real`); ("vec", `:num->real^N`);
538 ("%", `:real->real^N->real^N`); ("vector_neg", `:real^N->real^N`);
539 ("vector_sub", `:real^N->real^N->real^N`);
540 ("vector_add", `:real^N->real^N->real^N`); ("sqrt", `:real->real`);
541 ("hull", `:((A->bool)->bool)->(A->bool)->A->bool`);
542 ("inf", `:(real->bool)->real`); ("sup", `:(real->bool)->real`);
544 `:(A->A->bool)->((A->C)->B->bool)->(B->A)->((A->C)->B->C)->bool`);
546 `:(A->A->bool)->((A->B)->P->bool)->(P->A)->((A->B)->P->B)->bool`);
548 `:(B->A->bool)->((B->C)->D->bool)->(D->A)->((B->C)->D->E)->bool`);
549 ("CASEWISE", `:((A->C)#(B->A->D))list->B->C->D`);
550 ("vector", `:(A)list->A^N`);
551 ("dest_auto_define_finite_type_3", `:3->num`);
552 ("mk_auto_define_finite_type_3", `:num->3`);
553 ("dest_auto_define_finite_type_2", `:2->num`);
554 ("mk_auto_define_finite_type_2", `:num->2`);
555 ("sndcart", `:A^(M,N)finite_sum->A^N`);
556 ("fstcart", `:A^(M,N)finite_sum->A^M`);
557 ("pastecart", `:A^M->A^N->A^(M,N)finite_sum`);
558 ("dest_finite_sum", `:(A,B)finite_sum->num`);
559 ("mk_finite_sum", `:num->(A,B)finite_sum`); ("lambda", `:(num->A)->A^B`);
560 ("$", `:B^A->num->B`); ("dest_cart", `:A^B->(B)finite_image->A`);
561 ("mk_cart", `:((B)finite_image->A)->A^B`);
562 ("dest_finite_image", `:(A)finite_image->num`);
563 ("finite_index", `:num->(A)finite_image`);
564 ("dimindex", `:(A->bool)->num`); ("sum", `:(A->bool)->(A->real)->real`);
565 ("nsum", `:(A->bool)->(A->num)->num`);
566 ("iterate", `:(B->B->B)->(A->bool)->(A->B)->B`);
567 ("support", `:(B->B->B)->(A->B)->(A->bool)->A->bool`);
568 ("monoidal", `:(A->A->A)->bool`); ("neutral", `:(A->A->A)->A`);
569 ("..", `:num->num->num->bool`); ("COUNTABLE", `:(A->bool)->bool`);
570 (">_c", `:(A->bool)->(B->bool)->bool`);
571 (">=_c", `:(A->bool)->(B->bool)->bool`);
572 ("=_c", `:(A->bool)->(B->bool)->bool`);
573 ("<_c", `:(A->bool)->(B->bool)->bool`);
574 ("<=_c", `:(A->bool)->(B->bool)->bool`);
575 ("PAIRWISE", `:(A->A->bool)->(A)list->bool`);
576 ("pairwise", `:(A->A->bool)->(A->bool)->bool`);
577 ("list_of_set", `:(A->bool)->(A)list`);
578 ("set_of_list", `:(A)list->A->bool`);
579 ("CROSS", `:(A->bool)->(B->bool)->A#B->bool`);
580 ("HAS_SIZE", `:(A->bool)->num->bool`); ("CARD", `:(A->bool)->num`);
581 ("ITSET", `:(A->B->B)->(A->bool)->B->B`);
582 ("FINREC", `:(A->B->B)->B->(A->bool)->B->num->bool`);
583 ("REST", `:(A->bool)->A->bool`); ("CHOICE", `:(A->bool)->A`);
584 ("BIJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
585 ("SURJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
586 ("INJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
587 ("IMAGE", `:(A->B)->(A->bool)->B->bool`);
588 ("INFINITE", `:(A->bool)->bool`); ("FINITE", `:(A->bool)->bool`);
589 ("SING", `:(A->bool)->bool`); ("DISJOINT", `:(A->bool)->(A->bool)->bool`);
590 ("PSUBSET", `:(A->bool)->(A->bool)->bool`);
591 ("SUBSET", `:(A->bool)->(A->bool)->bool`);
592 ("DELETE", `:(A->bool)->A->A->bool`);
593 ("DIFF", `:(A->bool)->(A->bool)->A->bool`);
594 ("INTERS", `:((A->bool)->bool)->A->bool`);
595 ("INTER", `:(A->bool)->(A->bool)->A->bool`);
596 ("UNIONS", `:((A->bool)->bool)->A->bool`);
597 ("UNION", `:(A->bool)->(A->bool)->A->bool`); ("UNIV", `:A->bool`);
598 ("INSERT", `:A->(A->bool)->A->bool`); ("EMPTY", `:A->bool`);
599 ("SETSPEC", `:A->bool->A->bool`); ("GSPEC", `:(A->bool)->A->bool`);
600 ("IN", `:A->(A->bool)->bool`); ("num_gcd", `:num#num->num`);
601 ("num_coprime", `:num#num->bool`); ("num_mod", `:num->num->num->bool`);
602 ("num_divides", `:num->num->bool`); ("num_of_int", `:int->num`);
603 ("int_gcd", `:int#int->int`); ("int_coprime", `:int#int->bool`);
604 ("int_mod", `:int->int->int->bool`); ("int_divides", `:int->int->bool`);
605 ("real_mod", `:real->real->real->bool`);
606 ("==", `:A->A->(A->A->bool)->bool`); ("rem", `:int->int->int`);
607 ("div", `:int->int->int`); ("int_pow", `:int->num->int`);
608 ("int_min", `:int->int->int`); ("int_max", `:int->int->int`);
609 ("int_abs", `:int->int`); ("int_mul", `:int->int->int`);
610 ("int_sub", `:int->int->int`); ("int_add", `:int->int->int`);
611 ("int_neg", `:int->int`); ("int_of_num", `:num->int`);
612 ("int_gt", `:int->int->bool`); ("int_ge", `:int->int->bool`);
613 ("int_lt", `:int->int->bool`); ("int_le", `:int->int->bool`);
614 ("real_of_int", `:int->real`); ("int_of_real", `:real->int`);
615 ("is_int", `:real->bool`); ("DECIMAL", `:num->num->real`);
616 ("real_min", `:real->real->real`); ("real_max", `:real->real->real`);
617 ("real_div", `:real->real->real`); ("real_pow", `:real->num->real`);
618 ("real_abs", `:real->real`); ("real_gt", `:real->real->bool`);
619 ("real_ge", `:real->real->bool`); ("real_lt", `:real->real->bool`);
620 ("real_sub", `:real->real->real`); ("real_inv", `:real->real`);
621 ("real_le", `:real->real->bool`); ("real_mul", `:real->real->real`);
622 ("real_add", `:real->real->real`); ("real_neg", `:real->real`);
623 ("real_of_num", `:num->real`); ("dest_real", `:real->hreal#hreal->bool`);
624 ("mk_real", `:(hreal#hreal->bool)->real`);
625 ("treal_eq", `:hreal#hreal->hreal#hreal->bool`);
626 ("treal_inv", `:hreal#hreal->hreal#hreal`);
627 ("treal_le", `:hreal#hreal->hreal#hreal->bool`);
628 ("treal_mul", `:hreal#hreal->hreal#hreal->hreal#hreal`);
629 ("treal_add", `:hreal#hreal->hreal#hreal->hreal#hreal`);
630 ("treal_neg", `:hreal#hreal->hreal#hreal`);
631 ("treal_of_num", `:num->hreal#hreal`); ("hreal_inv", `:hreal->hreal`);
632 ("hreal_le", `:hreal->hreal->bool`);
633 ("hreal_mul", `:hreal->hreal->hreal`);
634 ("hreal_add", `:hreal->hreal->hreal`); ("hreal_of_num", `:num->hreal`);
635 ("dest_hreal", `:hreal->nadd->bool`);
636 ("mk_hreal", `:(nadd->bool)->hreal`); ("nadd_inv", `:nadd->nadd`);
637 ("nadd_rinv", `:nadd->num->num`); ("nadd_mul", `:nadd->nadd->nadd`);
638 ("nadd_add", `:nadd->nadd->nadd`); ("nadd_le", `:nadd->nadd->bool`);
639 ("nadd_of_num", `:num->nadd`); ("nadd_eq", `:nadd->nadd->bool`);
640 ("dest_nadd", `:nadd->num->num`); ("mk_nadd", `:(num->num)->nadd`);
641 ("is_nadd", `:(num->num)->bool`); ("dist", `:num#num->num`);
642 ("ASCII", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
643 ("_16756", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
644 ("_dest_char", `:char->(bool#bool#bool#bool#bool#bool#bool#bool)recspace`);
645 ("_mk_char", `:(bool#bool#bool#bool#bool#bool#bool#bool)recspace->char`);
646 ("ZIP", `:(A)list->(B)list->(A#B)list`);
647 ("ITLIST2", `:(A->B->C->C)->(A)list->(B)list->C->C`);
648 ("ASSOC", `:A->(A#B)list->B`); ("FILTER", `:(A->bool)->(A)list->(A)list`);
649 ("EL", `:num->(A)list->A`);
650 ("MAP2", `:(A->B->C)->(A)list->(B)list->(C)list`);
651 ("ALL2", `:(A->B->bool)->(A)list->(B)list->bool`);
652 ("MEM", `:A->(A)list->bool`); ("ITLIST", `:(A->B->B)->(A)list->B->B`);
653 ("EX", `:(A->bool)->(A)list->bool`); ("ALL", `:(A->bool)->(A)list->bool`);
654 ("NULL", `:(A)list->bool`); ("REPLICATE", `:num->A->(A)list`);
655 ("LAST", `:(A)list->A`); ("MAP", `:(A->B)->(A)list->(B)list`);
656 ("LENGTH", `:(A)list->num`); ("REVERSE", `:(A)list->(A)list`);
657 ("APPEND", `:(A)list->(A)list->(A)list`); ("TL", `:(A)list->(A)list`);
658 ("HD", `:(A)list->A`); ("ISO", `:(A->B)->(B->A)->bool`);
659 ("CONS", `:A->(A)list->(A)list`); ("NIL", `:(A)list`);
660 ("_dest_list", `:(A)list->(A)recspace`);
661 ("_mk_list", `:(A)recspace->(A)list`); ("SOME", `:A->(A)option`);
662 ("NONE", `:(A)option`); ("_dest_option", `:(A)option->(A)recspace`);
663 ("_mk_option", `:(A)recspace->(A)option`); ("OUTR", `:A+B->B`);
664 ("OUTL", `:A+B->A`); ("INR", `:B->A+B`); ("INL", `:A->A+B`);
665 ("_dest_sum", `:A+B->(A#B)recspace`); ("_mk_sum", `:(A#B)recspace->A+B`);
666 ("FNIL", `:num->A`); ("FCONS", `:A->(num->A)->num->A`);
667 ("CONSTR", `:num->A->(num->(A)recspace)->(A)recspace`);
668 ("BOTTOM", `:(A)recspace`); ("_dest_rec", `:(A)recspace->num->A->bool`);
669 ("_mk_rec", `:(num->A->bool)->(A)recspace`);
670 ("ZRECSPACE", `:(num->A->bool)->bool`); ("ZBOT", `:num->A->bool`);
671 ("ZCONSTR", `:num->A->(num->num->A->bool)->num->A->bool`);
672 ("INJP", `:(num->A->bool)->(num->A->bool)->num->A->bool`);
673 ("INJF", `:(num->num->A->bool)->num->A->bool`);
674 ("INJA", `:A->num->A->bool`); ("INJN", `:num->num->A->bool`);
675 ("NUMRIGHT", `:num->num`); ("NUMLEFT", `:num->bool`);
676 ("NUMSUM", `:bool->num->num`); ("NUMSND", `:num->num`);
677 ("NUMFST", `:num->num`); ("NUMPAIR", `:num->num->num`);
678 ("MEASURE", `:(A->num)->A->A->bool`); ("WF", `:(A->A->bool)->bool`);
679 ("minimal", `:(num->bool)->num`); ("MIN", `:num->num->num`);
680 ("MAX", `:num->num->num`); ("MOD", `:num->num->num`);
681 ("DIV", `:num->num->num`); ("FACT", `:num->num`); ("-", `:num->num->num`);
682 ("ODD", `:num->bool`); ("EVEN", `:num->bool`); (">", `:num->num->bool`);
683 (">=", `:num->num->bool`); ("<", `:num->num->bool`);
684 ("<=", `:num->num->bool`); ("EXP", `:num->num->num`);
685 ("*", `:num->num->num`); ("BIT1", `:num->num`); ("BIT0", `:num->num`);
686 ("+", `:num->num->num`); ("PRE", `:num->num`); ("NUMERAL", `:num->num`);
687 ("SUC", `:num->num`); ("_0", `:num`); ("dest_num", `:num->ind`);
688 ("mk_num", `:ind->num`); ("NUM_REP", `:ind->bool`); ("IND_0", `:ind`);
689 ("IND_SUC", `:ind->ind`); ("ONTO", `:(A->B)->bool`);
690 ("ONE_ONE", `:(A->B)->bool`); ("PASSOC", `:((A#B)#C->D)->A#B#C->D`);
691 ("UNCURRY", `:(A->B->C)->A#B->C`); ("CURRY", `:(A#B->C)->A->B->C`);
692 ("SND", `:A#B->B`); ("FST", `:A#B->A`); (",", `:A->B->A#B`);
693 ("REP_prod", `:A#B->A->B->bool`); ("ABS_prod", `:(A->B->bool)->A#B`);
694 ("mk_pair", `:A->B->A->B->bool`); ("_FUNCTION", `:(A->B->bool)->A->B`);
695 ("_MATCH", `:A->(A->B->bool)->B`);
696 ("_GUARDED_PATTERN", `:bool->bool->bool->bool`);
697 ("_UNGUARDED_PATTERN", `:bool->bool->bool`);
698 ("_SEQPATTERN", `:(A->B->bool)->(A->B->bool)->A->B->bool`);
699 ("GEQ", `:A->A->bool`); ("GABS", `:(A->bool)->A`); ("LET_END", `:A->A`);
700 ("LET", `:(A->B)->A->B`); ("one", `:1`); ("one_REP", `:1->bool`);
701 ("one_ABS", `:bool->1`); ("I", `:A->A`); ("o", `:(B->C)->(A->B)->A->C`);
702 ("COND", `:bool->A->A->A`); ("@", `:(A->bool)->A`);
703 ("_FALSITY_", `:bool`); ("?!", `:(A->bool)->bool`); ("~", `:bool->bool`);
704 ("F", `:bool`); ("\\/", `:bool->bool->bool`); ("?", `:(A->bool)->bool`);
705 ("!", `:(A->bool)->bool`); ("==>", `:bool->bool->bool`);
706 ("/\\", `:bool->bool->bool`); ("T", `:bool`); ("=", `:A->A->bool`)];;
707 let the_loaded_files =
708 ["flyspeck_utility.hl"; "update_database_310.ml"; "hypermap.hl"; "vol1.hl";
709 "trigonometry.hl"; "database2194fe.ml"; "flyspeck_utility.hl"; "trig2.hl";
710 "trig1.hl"; "ineqdata3q1h.hl"; "ineq.hl"; "enclosed_def.hl";
711 "quadratic_root_plus_def.hl"; "abc_of_quadratic_def.hl"; "muR_def.hl";
712 "collect_geom.hl"; "cayleyR_def.hl"; "affprops.hl"; "AFF_SGN_TAC.hl";
713 "geomdetail.hl"; "snapshot.hl"; "snapshot.hl"; "snapshot.hl";
714 "snapshot.hl"; "snapshot.hl"; "sphere.hl"; "prove_by_refinement.hl";
715 "update_database_310.ml"; "database3be71a.ml"; "snapshot.hl";
716 "print-types.ml"; "flyspeck.ml"; "wlog_examples.ml"; "wlog.ml"; "real.ml";
717 "measure.ml"; "card.ml"; "wo.ml"; "geom.ml"; "transc.ml"; "canal.ml";
718 "complex.ml"; "integration.ml"; "analysis.ml"; "dimension.ml";
719 "convex.ml"; "topology.ml"; "iter.ml"; "floor.ml"; "cross.ml";
720 "determinants.ml"; "products.ml"; "permutations.ml"; "vectors.ml";
721 "misc.ml"; "database.ml"; "help.ml"; "define.ml"; "cart.ml"; "iter.ml";
722 "sets.ml"; "int.ml"; "calc_rat.ml"; "real.ml"; "realarith.ml";
723 "calc_int.ml"; "realax.ml"; "list.ml"; "ind-types.ml"; "grobner.ml";
724 "normalizer.ml"; "calc_num.ml"; "wf.ml"; "arith.ml"; "num.ml"; "pair.ml";
725 "recursion.ml"; "quot.ml"; "meson.ml"; "canon.ml"; "trivia.ml";
726 "class.ml"; "ind-defs.ml"; "theorems.ml"; "simp.ml"; "itab.ml";
727 "tactics.ml"; "drule.ml"; "bool.ml"; "equal.ml"; "printer.ml";
728 "parser.ml"; "preterm.ml"; "nets.ml"; "basics.ml"; "fusion.ml"; "lib.ml";
730 let the_types = [("loop", 1); ("hypermap", 1); ("net", 1); ("topology", 1); ("3", 0);
731 ("2", 0); ("finite_sum", 2); ("cart", 2); ("finite_image", 1); ("int", 0);
732 ("real", 0); ("hreal", 0); ("nadd", 0); ("char", 0); ("list", 1);
733 ("option", 1); ("sum", 2); ("recspace", 1); ("num", 0); ("ind", 0);
734 ("prod", 2); ("1", 0); ("bool", 0); ("fun", 2)];;
735 let the_overload_skeletons = Snapshot_v220_7_31_2009.the_overload_skeletons;;