development/thales/chaff/general/flyshot.hl

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