development/thales/chaff/general/snapshot.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: General                                                 *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-10                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 store data from different HOL Light snapshots to make it easier to make
  11 an upgrade from one snapshot to the next.
  12 *)
  13
  14
  15
  16 module type Snapshot_type = sig
  17   val the_constants :  (string * hol_type) list
  18   val the_loaded_files : string list
  19   val the_overload_skeletons : (string*hol_type) list
  20   val the_interface : (string * (string * hol_type)) list
  21   val the_types:(string*int) list
  22 end;;
  23
  24 module Snapshot_utility = struct
  25
  26 (* This was used to make printable manufactured types.  No more `:?467346` *)
  27
  28 let clean_ty ty =
  29    let fr = (union (tyvars ty) []) in
  30    let alpha = map (mk_vartype o (String.make 1) o (char_of_int)) (65--(65+List.length(fr))) in
  31    let  alphafr = subtract alpha fr in
  32    let sel = filter (fun t ->  (dest_vartype t).[0]='?')  fr in
  33    type_subst (map (fun t-> (List.nth alphafr t,List.nth sel t)) (0--(List.length sel - 1))) ty;;
  34
  35 (*
  36 0;;
  37 #print_length 10000;;
  38 map (fun (t,u) -> (t, clean_ty u)) (constants());;
  39 map fst !loaded_files;;
  40 !the_overload_skeletons;;
  41 map (fun (t,(u,v)) -> (t,(u,clean_ty v))) (!the_interface);;
  42 types();;
  43 #print_length 500;;
  44 *)
  45
  46 end;;
  47
  48
  49 module Snapshot_v220_7_29_2009 : Snapshot_type = struct
  50
  51   let the_types =  [("net", 1); ("topology", 1); ("3", 0); ("2", 0); ("finite_sum", 2);
  52    ("cart", 2); ("finite_image", 1); ("int", 0); ("real", 0); ("hreal", 0);
  53    ("nadd", 0); ("char", 0); ("list", 1); ("option", 1); ("sum", 2);
  54    ("recspace", 1); ("num", 0); ("ind", 0); ("prod", 2); ("1", 0);
  55    ("bool", 0); ("fun", 2)];;
  56
  57   let the_loaded_files =  ["flyspeck.ml"; "wlog_examples.ml"; "wlog.ml"; "real.ml"; "measure.ml";
  58    "card.ml"; "wo.ml"; "geom.ml"; "transc.ml"; "canal.ml"; "complex.ml";
  59    "integration.ml"; "analysis.ml"; "dimension.ml"; "convex.ml";
  60    "topology.ml"; "iter.ml"; "floor.ml"; "cross.ml"; "determinants.ml";
  61    "products.ml"; "permutations.ml"; "vectors.ml"; "misc.ml"; "database.ml";
  62    "help.ml"; "define.ml"; "cart.ml"; "iter.ml"; "sets.ml"; "int.ml";
  63    "calc_rat.ml"; "real.ml"; "realarith.ml"; "calc_int.ml"; "realax.ml";
  64    "list.ml"; "ind-types.ml"; "grobner.ml"; "normalizer.ml"; "calc_num.ml";
  65    "wf.ml"; "arith.ml"; "num.ml"; "pair.ml"; "recursion.ml"; "quot.ml";
  66    "meson.ml"; "canon.ml"; "trivia.ml"; "class.ml"; "ind-defs.ml";
  67    "theorems.ml"; "simp.ml"; "itab.ml"; "tactics.ml"; "drule.ml"; "bool.ml";
  68    "equal.ml"; "printer.ml"; "parser.ml"; "preterm.ml"; "nets.ml";
  69    "basics.ml"; "fusion.ml"; "lib.ml"; "sys.ml"];;
  70
  71   let the_overload_skeletons =
  72     [("real_interval", `:A`); ("segment", `:A`); ("interval", `:A`);
  73    ("**", `:A->B->C`); ("norm", `:A->real`); ("gcd", `:A#A->A`);
  74    ("coprime", `:A#A->bool`); ("mod", `:A->A->A->bool`);
  75    ("divides", `:A->A->bool`); ("&", `:num->A`); ("min", `:A->A->A`);
  76    ("max", `:A->A->A`); ("abs", `:A->A`); ("inv", `:A->A`);
  77    ("pow", `:A->num->A`); ("--", `:A->A`); (">=", `:A->A->bool`);
  78    (">", `:A->A->bool`); ("<=", `:A->A->bool`); ("<", `:A->A->bool`);
  79    ("/", `:A->A->A`); ("*", `:A->A->A`); ("-", `:A->A->A`);
  80    ("+", `:A->A->A`)];;
  81
  82 (* this should be regenerated. It was not captured at the right moment *)
  83   let the_interface =
  84   [("+", ("real_add", `:real->real->real`));
  85    ("-", ("real_sub", `:real->real->real`));
  86    ("*", ("real_mul", `:real->real->real`));
  87    ("/", ("real_div", `:real->real->real`));
  88    ("<", ("real_lt", `:real->real->bool`));
  89    ("<=", ("real_le", `:real->real->bool`));
  90    (">", ("real_gt", `:real->real->bool`));
  91    (">=", ("real_ge", `:real->real->bool`));
  92    ("--", ("real_neg", `:real->real`));
  93    ("pow", ("real_pow", `:real->num->real`));
  94    ("inv", ("real_inv", `:real->real`));
  95    ("abs", ("real_abs", `:real->real`));
  96    ("max", ("real_max", `:real->real->real`));
  97    ("min", ("real_min", `:real->real->real`));
  98    ("&", ("real_of_num", `:num->real`));
  99    ("mod", ("real_mod", `:real->real->real->bool`));
 100    ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
 101    ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
 102    ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
 103    (">=", (">=", `:num->num->bool`));
 104    ("divides", ("num_divides", `:num->num->bool`));
 105    ("mod", ("num_mod", `:num->num->num->bool`));
 106    ("coprime", ("num_coprime", `:num#num->bool`));
 107    ("gcd", ("num_gcd", `:num#num->num`));
 108    ("vol", ("measure", `:(real^3->bool)->real`));
 109    ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
 110    ("+", ("vector_add", `:real^N->real^N->real^N`));
 111    ("-", ("vector_sub", `:real^N->real^N->real^N`));
 112    ("--", ("vector_neg", `:real^N->real^N`));
 113    ("norm", ("vector_norm", `:real^N->real`));
 114    ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
 115    ("real_interval",
 116     ("closed_real_interval", `:(real#real)list->real->bool`));
 117    ("real_interval", ("open_real_interval", `:real#real->real->bool`));
 118    ("inv", ("complex_inv", `:real^2->real^2`));
 119    ("pow", ("complex_pow", `:real^2->num->real^2`));
 120    ("/", ("complex_div", `:real^2->real^2->real^2`));
 121    ("*", ("complex_mul", `:real^2->real^2->real^2`));
 122    ("-", ("vector_sub", `:real^2->real^2->real^2`));
 123    ("+", ("vector_add", `:real^2->real^2->real^2`));
 124    ("--", ("vector_neg", `:real^2->real^2`));
 125    ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
 126    ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
 127    ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
 128    ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
 129    ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
 130    ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
 131    ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
 132    ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
 133    ("--", ("matrix_neg", `:real^N^M->real^N^M`));
 134    ("dist", ("distance", `:real^N#real^N->real`));
 135    ("gcd", ("int_gcd", `:int#int->int`));
 136    ("coprime", ("int_coprime", `:int#int->bool`));
 137    ("mod", ("int_mod", `:int->int->int->bool`));
 138    ("divides", ("int_divides", `:int->int->bool`));
 139    ("&", ("int_of_num", `:num->int`));
 140    ("min", ("int_min", `:int->int->int`));
 141    ("max", ("int_max", `:int->int->int`)); ("abs", ("int_abs", `:int->int`));
 142    ("pow", ("int_pow", `:int->num->int`)); ("--", ("int_neg", `:int->int`));
 143    (">=", ("int_ge", `:int->int->bool`));
 144    (">", ("int_gt", `:int->int->bool`));
 145    ("<=", ("int_le", `:int->int->bool`));
 146    ("<", ("int_lt", `:int->int->bool`));
 147    ("*", ("int_mul", `:int->int->int`));
 148    ("-", ("int_sub", `:int->int->int`));
 149    ("+", ("int_add", `:int->int->int`));
 150    ("&", ("hreal_of_num", `:num->hreal`));
 151    ("<=>", ("=", `:bool->bool->bool`))];;
 152
 153   let the_constants =
 154   [("SDIFF", `:(A->bool)->(A->bool)->A->bool`);
 155    ("vol_ball_wedge", `:real^3->real^3->real^3->real^3->real->real`);
 156    ("vol_rect", `:real^A->real^B->real`);
 157    ("vol_conv", `:real^A->real^A->real^A->real^A->real`);
 158    ("vol_conic_cap_wedge",
 159     `:real^3->real^3->real^3->real^3->real->real->real`);
 160    ("vol_frustt_wedge", `:real^3->real^3->real^3->real^3->real->real->real`);
 161    ("vol_solid_triangle", `:real^A->real^A->real^A->real^A->real->real`);
 162    ("primitive", `:(real^3->bool)->bool`);
 163    ("circular_cone", `:(real^3->bool)->bool`);
 164    ("c_cone", `:real^3#real^3#real->real^3->bool`);
 165    ("sphere", `:(real^3->bool)->bool`);
 166    ("rect", `:real^3->real^3->real^3->bool`);
 167    ("solid_triangle", `:real^A->(real^A->bool)->real->real^A->bool`);
 168    ("cone0", `:real^A->(real^A->bool)->real^A->bool`);
 169    ("cone", `:real^A->(real^A->bool)->real^A->bool`);
 170    ("dihV", `:real^A->real^A->real^A->real^A->real`);
 171    ("opposite", `:real^N->real^N->(real^N->bool)->bool`);
 172    ("arcV", `:real^A->real^A->real^A->real`);
 173    ("wedge", `:real^3->real^3->real^3->real^3->real^3->bool`);
 174    ("azim", `:real^3->real^3->real^3->real^3->real`);
 175    ("orthonormal", `:real^3->real^3->real^3->bool`);
 176    ("conic_cap", `:real^A->real^A->real->real->real^A->bool`);
 177    ("ellipsoid", `:real^3->real->real^3->bool`);
 178    ("normball", `:real^A->real->real^A->bool`);
 179    ("scale", `:real^3->real^3->real^3`);
 180    ("frustt", `:real^A->real^A->real->real->real^A->bool`);
 181    ("frustum", `:real^N->real^N->real->real->real->real^N->bool`);
 182    ("rcone_eq", `:real^A->real^A->real->real^A->bool`);
 183    ("rcone_ge", `:real^A->real^A->real->real^A->bool`);
 184    ("rcone_gt", `:real^A->real^A->real->real^A->bool`);
 185    ("rconesgn", `:(real->real->bool)->real^A->real^A->real->real^A->bool`);
 186    ("delta_x", `:real->real->real->real->real->real->real`);
 187    ("conv0", `:(real^A->bool)->real^A->bool`);
 188    ("aff_le", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 189    ("aff_lt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 190    ("aff_ge", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 191    ("aff_gt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 192    ("sgn_le", `:real->bool`); ("sgn_lt", `:real->bool`);
 193    ("sgn_ge", `:real->bool`); ("sgn_gt", `:real->bool`);
 194    ("affsign", `:(real->bool)->(real^A->bool)->(real^A->bool)->real^A->bool`);
 195    ("lin_combo", `:(real^N->bool)->(real^N->real)->real^N`);
 196    ("pad2d3d", `:real^2->real^3`); ("plane", `:(real^A->bool)->bool`);
 197    ("slice", `:num->real->(real^A->bool)->real^B->bool`);
 198    ("pushin", `:num->B->B^A->B^C`); ("dropout", `:num->real^N->real^M`);
 199    ("real_measure", `:(real->bool)->real`);
 200    ("real_measurable", `:(real->bool)->bool`);
 201    ("has_real_measure", `:(real->bool)->real->bool`);
 202    ("absolutely_real_integrable_on", `:(real->real)->(real->bool)->bool`);
 203    ("real_negligible", `:(real->bool)->bool`);
 204    ("real_integral", `:(real->bool)->(real->real)->real`);
 205    ("real_integrable_on", `:(real->real)->(real->bool)->bool`);
 206    ("has_real_integral", `:(real->real)->real->(real->bool)->bool`);
 207    ("closed_real_interval", `:(real#real)list->real->bool`);
 208    ("open_real_interval", `:real#real->real->bool`);
 209    ("is_realinterval", `:(real->bool)->bool`);
 210    ("real_differentiable_on", `:(real->real)->(real->bool)->bool`);
 211    ("higher_real_derivative", `:num->(real->real)->real->real`);
 212    ("real_derivative", `:(real->real)->real->real`);
 213    ("real_differentiable", `:(real->real)->(real)net->bool`);
 214    ("has_real_derivative", `:(real->real)->real->(real)net->bool`);
 215    ("real_continuous_on", `:(real->real)->(real->bool)->bool`);
 216    ("real_continuous", `:(A->real)->(A)net->bool`);
 217    ("at_neginfinity", `:(real)net`); ("at_posinfinity", `:(real)net`);
 218    ("atreal", `:real->(real)net`);
 219    ("real_summable", `:(num->bool)->(num->real)->bool`);
 220    ("real_infsum", `:(num->bool)->(num->real)->real`);
 221    ("real_sums", `:(num->real)->real->(num->bool)->bool`);
 222    ("--->", `:(A->real)->real->(A)net->bool`);
 223    ("real_compact", `:(real->bool)->bool`);
 224    ("real_bounded", `:(real->bool)->bool`);
 225    ("euclideanreal", `:(real)topology`);
 226    ("real_closed", `:(real->bool)->bool`);
 227    ("real_open", `:(real->bool)->bool`);
 228    ("measure", `:(real^A->bool)->real`);
 229    ("measurable", `:(real^A->bool)->bool`);
 230    ("has_measure", `:(real^A->bool)->real->bool`);
 231    ("*_c", `:(A->bool)->(B->bool)->A#B->bool`);
 232    ("+_c", `:(A->bool)->(B->bool)->A+B->bool`);
 233    ("ordinal", `:(A#A->bool)->bool`);
 234    ("linseg", `:(A#A->bool)->A->A#A->bool`);
 235    ("inseg", `:(A#A->bool)->(A#A->bool)->bool`);
 236    ("woset", `:(A#A->bool)->bool`);
 237    ("chain", `:(A#A->bool)->(A->bool)->bool`);
 238    ("poset", `:(A#A->bool)->bool`); ("fl", `:(A#A->bool)->A->bool`);
 239    ("less", `:(A#A->bool)->A#A->bool`);
 240    ("angle", `:real^A#real^A#real^A->real`);
 241    ("vector_angle", `:real^A->real^A->real`); ("acs", `:real->real`);
 242    ("asn", `:real->real`); ("cacs", `:real^2->real^2`);
 243    ("casn", `:real^2->real^2`); ("atn", `:real->real`);
 244    ("catn", `:real^2->real^2`); ("unwinding", `:real^2->real^2`);
 245    ("cpow", `:real^2->real^2->real^2`); ("clog", `:real^2->real^2`);
 246    ("tan", `:real->real`); ("ctan", `:real^2->real^2`);
 247    ("rotate2d", `:real->real^2->real^2`); ("Arg", `:real^2->real`);
 248    ("pi", `:real`); ("log", `:real->real`); ("cos", `:real->real`);
 249    ("sin", `:real->real`); ("exp", `:real->real`);
 250    ("csin", `:real^2->real^2`); ("ccos", `:real^2->real^2`);
 251    ("cexp", `:real^2->real^2`);
 252    ("analytic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
 253    ("holomorphic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
 254    ("higher_complex_derivative", `:num->(real^2->real^2)->real^2->real^2`);
 255    ("complex_derivative", `:(real^2->real^2)->real^2->real^2`);
 256    ("complex_differentiable", `:(real^2->real^2)->(real^2)net->bool`);
 257    ("has_complex_derivative", `:(real^2->real^2)->real^2->(real^2)net->bool`);
 258    ("cproduct", `:(A->bool)->(A->real^2)->real^2`);
 259    ("real", `:real^2->bool`); ("csqrt", `:real^2->real^2`);
 260    ("cnj", `:real^2->real^2`); ("complex_pow", `:real^2->num->real^2`);
 261    ("complex_div", `:real^2->real^2->real^2`);
 262    ("complex_inv", `:real^2->real^2`);
 263    ("complex_mul", `:real^2->real^2->real^2`); ("ii", `:real^2`);
 264    ("Cx", `:real->real^2`); ("complex", `:real#real->real^2`);
 265    ("Im", `:real^2->real`); ("Re", `:real^2->real`);
 266    ("absolutely_integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 267    ("negligible", `:(real^A->bool)->bool`);
 268    ("indicator", `:(real^M->bool)->real^M->real^1`);
 269    ("division_points",
 270     `:(real^N->bool)->((real^N->bool)->bool)->num#real->bool`);
 271    ("lifted", `:(A->A->B)->(A)option->(A)option->(B)option`);
 272    ("operative", `:(A->A->A)->((real^N->bool)->A)->bool`);
 273    ("integral", `:(real^A->bool)->(real^A->real^B)->real^B`);
 274    ("integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 275    ("has_integral", `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
 276    ("has_integral_compact_interval",
 277     `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
 278    ("fine", `:(A->B->bool)->(A#(B->bool)->bool)->bool`);
 279    ("tagged_division_of",
 280     `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
 281    ("tagged_partial_division_of",
 282     `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
 283    ("division_of", `:((real^A->bool)->bool)->(real^A->bool)->bool`);
 284    ("gauge", `:(real^A->real^A->bool)->bool`);
 285    ("content", `:(real^M->bool)->real`);
 286    ("interval_lowerbound", `:(real^M->bool)->real^M`);
 287    ("interval_upperbound", `:(real^M->bool)->real^M`);
 288    ("vector_derivative", `:(real^1->real^N)->(real^1)net->real^N`);
 289    ("has_vector_derivative", `:(real^1->real^A)->real^A->(real^1)net->bool`);
 290    ("jacobian", `:(real^A->real^B)->(real^A)net->real^A^B`);
 291    ("frechet_derivative", `:(real^A->real^B)->(real^A)net->real^A->real^B`);
 292    ("differentiable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 293    ("differentiable", `:(real^B->real^A)->(real^B)net->bool`);
 294    ("has_derivative",
 295     `:(real^B->real^A)->(real^B->real^A)->(real^B)net->bool`);
 296    ("interval_bij", `:real^N#real^N->real^N#real^N->real^N->real^N`);
 297    ("retract_of", `:(real^A->bool)->(real^A->bool)->bool`);
 298    ("retraction", `:(real^N->bool)#(real^N->bool)->(real^N->real^N)->bool`);
 299    ("reduced", `:((num->num)->num->num)->num->(num->num)->num`);
 300    ("ksimplex", `:num->num->((num->num)->bool)->bool`);
 301    ("kle", `:num->(num->num)->(num->num)->bool`);
 302    ("path_connected", `:(real^A->bool)->bool`);
 303    ("path_component", `:(real^A->bool)->real^A->real^A->bool`);
 304    ("linepath", `:real^A#real^A->real^1->real^A`);
 305    ("shiftpath", `:real^1->(real^1->real^N)->real^1->real^N`);
 306    ("arc", `:(real^1->real^N)->bool`);
 307    ("simple_path", `:(real^1->real^N)->bool`);
 308    ("++", `:(real^1->A)->(real^1->A)->real^1->A`);
 309    ("reversepath", `:(real^1->real^N)->real^1->real^N`);
 310    ("path_image", `:(real^1->real^N)->real^N->bool`);
 311    ("pathfinish", `:(real^1->real^N)->real^N`);
 312    ("pathstart", `:(real^1->real^N)->real^N`);
 313    ("path", `:(real^1->real^N)->bool`);
 314    ("extreme_point_of", `:real^A->(real^A->bool)->bool`);
 315    ("face_of", `:(real^A->bool)->(real^A->bool)->bool`);
 316    ("relative_interior", `:(real^A->bool)->real^A->bool`);
 317    ("starlike", `:(real^A->bool)->bool`);
 318    ("epigraph",
 319     `:(real^N->bool)->(real^N->real)->real^(N,1)finite_sum->bool`);
 320    ("convex_on", `:(real^A->real)->(real^A->bool)->bool`);
 321    ("coplanar", `:(real^A->bool)->bool`);
 322    ("affine_dependent", `:(real^N->bool)->bool`);
 323    ("conic", `:(real^A->bool)->bool`); ("convex", `:(real^A->bool)->bool`);
 324    ("affine", `:(real^A->bool)->bool`);
 325    ("closest_point", `:(real^A->bool)->real^A->real^A`);
 326    ("from", `:num->num->bool`);
 327    ("summable", `:(num->bool)->(num->real^A)->bool`);
 328    ("infsum", `:(num->bool)->(num->real^A)->real^A`);
 329    ("sums", `:(num->real^A)->real^A->(num->bool)->bool`);
 330    ("homeomorphic", `:(real^A->bool)->(real^B->bool)->bool`);
 331    ("homeomorphism",
 332     `:(real^B->bool)#(real^A->bool)->(real^B->real^A)#(real^A->real^B)->bool`);
 333    ("open_segment", `:real^A#real^A->real^A->bool`);
 334    ("closed_segment", `:(real^A#real^A)list->real^A->bool`);
 335    ("is_interval", `:(real^N->bool)->bool`);
 336    ("closed_interval", `:(real^N#real^N)list->real^N->bool`);
 337    ("open_interval", `:real^N#real^N->real^N->bool`);
 338    ("diameter", `:(real^A->bool)->real`);
 339    ("connected_component", `:(real^A->bool)->real^A->real^A->bool`);
 340    ("uniformly_continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 341    ("continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 342    ("continuous", `:(B->real^A)->(B)net->bool`);
 343    ("complete", `:(real^N->bool)->bool`); ("cauchy", `:(num->real^N)->bool`);
 344    ("compact", `:(real^N->bool)->bool`);
 345    ("bounded", `:(real^N->bool)->bool`); ("netlimit", `:(A)net->A`);
 346    ("lim", `:(A)net->(A->real^B)->real^B`);
 347    ("-->", `:(B->real^A)->real^A->(B)net->bool`);
 348    ("eventually", `:(A->bool)->(A)net->bool`);
 349    ("trivial_limit", `:(A)net->bool`);
 350    ("in_direction", `:real^A->real^A->(real^A)net`);
 351    ("within", `:(A)net->(A->bool)->(A)net`); ("sequentially", `:(num)net`);
 352    ("at_infinity", `:(real^A)net`); ("at", `:real^A->(real^A)net`);
 353    ("netord", `:(A)net->A->A->bool`); ("mk_net", `:(A->A->bool)->(A)net`);
 354    ("frontier", `:(real^A->bool)->real^A->bool`);
 355    ("closure", `:(real^A->bool)->real^A->bool`);
 356    ("interior", `:(real^A->bool)->real^A->bool`);
 357    ("limit_point_of", `:real^A->(real^A->bool)->bool`);
 358    ("connected", `:(real^A->bool)->bool`);
 359    ("cball", `:real^A#real->real^A->bool`);
 360    ("ball", `:real^A#real->real^A->bool`);
 361    ("euclidean", `:(real^A)topology`); ("closed", `:(real^N->bool)->bool`);
 362    ("open", `:(real^A->bool)->bool`);
 363    ("subtopology", `:(A)topology->(A->bool)->(A)topology`);
 364    ("closed_in", `:(A)topology->(A->bool)->bool`);
 365    ("topspace", `:(A)topology->A->bool`);
 366    ("open_in", `:(A)topology->(A->bool)->bool`);
 367    ("topology", `:((A->bool)->bool)->(A)topology`);
 368    ("istopology", `:((A->bool)->bool)->bool`);
 369    ("ITER", `:num->(A->A)->A->A`); ("frac", `:real->real`);
 370    ("floor", `:real->real`); ("integer", `:real->bool`);
 371    ("cross", `:real^3->real^3->real^3`);
 372    ("rotoinversion_matrix", `:real^A^A->bool`);
 373    ("rotation_matrix", `:real^A^A->bool`);
 374    ("orthogonal_matrix", `:real^N^N->bool`);
 375    ("orthogonal_transformation", `:(real^N->real^N)->bool`);
 376    ("det", `:real^N^N->real`); ("trace", `:real^N^N->real`);
 377    ("product", `:(A->bool)->(A->real)->real`); ("sign", `:(A->A)->real`);
 378    ("evenperm", `:(A->A)->bool`); ("permutation", `:(A->A)->bool`);
 379    ("swapseq", `:num->(A->A)->bool`); ("swap", `:A#A->A->A`);
 380    ("inverse", `:(B->A)->A->B`); ("permutes", `:(A->A)->(A->bool)->bool`);
 381    ("midpoint", `:real^A#real^A->real^A`);
 382    ("between", `:real^A->real^A#real^A->bool`);
 383    ("collinear", `:(real^A->bool)->bool`); ("infnorm", `:real^N->real`);
 384    ("rank", `:real^M^N->num`); ("columnvector", `:real^N->real^1^N`);
 385    ("rowvector", `:real^N->real^N^1`); ("dim", `:(real^A->bool)->num`);
 386    ("independent", `:(real^A->bool)->bool`);
 387    ("dependent", `:(real^A->bool)->bool`);
 388    ("span", `:(real^A->bool)->real^A->bool`);
 389    ("subspace", `:(real^A->bool)->bool`); ("drop", `:real^1->real`);
 390    ("lift", `:real->real^1`); ("onorm", `:(real^M->real^N)->real`);
 391    ("matrix", `:(real^M->real^N)->real^M^N`);
 392    ("matrix_inv", `:real^N^M->real^M^N`); ("invertible", `:real^N^M->bool`);
 393    ("columns", `:real^N^M->real^M->bool`);
 394    ("rows", `:real^N^M->real^N->bool`); ("column", `:num->real^N^M->real^M`);
 395    ("row", `:num->real^N^M->real^N`); ("transp", `:real^N^M->real^M^N`);
 396    ("mat", `:num->real^N^M`);
 397    ("vector_matrix_mul", `:real^M->real^N^M->real^N`);
 398    ("matrix_vector_mul", `:real^N^M->real^N->real^M`);
 399    ("matrix_mul", `:real^N^M->real^P^N->real^P^M`);
 400    ("matrix_sub", `:real^N^M->real^N^M->real^N^M`);
 401    ("matrix_add", `:real^N^M->real^N^M->real^N^M`);
 402    ("matrix_neg", `:real^N^M->real^N^M`);
 403    ("adjoint", `:(real^M->real^N)->real^N->real^M`);
 404    ("bilinear", `:(real^A->real^B->real^C)->bool`);
 405    ("linear", `:(real^M->real^N)->bool`);
 406    ("orthogonal", `:real^A->real^A->bool`); ("basis", `:num->real^A`);
 407    ("vsum", `:(A->bool)->(A->real^N)->real^N`);
 408    ("distance", `:real^A#real^A->real`); ("vector_norm", `:real^A->real`);
 409    ("dot", `:real^N->real^N->real`); ("vec", `:num->real^N`);
 410    ("%", `:real->real^N->real^N`); ("vector_neg", `:real^N->real^N`);
 411    ("vector_sub", `:real^N->real^N->real^N`);
 412    ("vector_add", `:real^N->real^N->real^N`); ("sqrt", `:real->real`);
 413    ("hull", `:((A->bool)->bool)->(A->bool)->A->bool`);
 414    ("inf", `:(real->bool)->real`); ("sup", `:(real->bool)->real`);
 415    ("superadmissible",
 416     `:(A->A->bool)->((A->C)->B->bool)->(B->A)->((A->C)->B->C)->bool`);
 417    ("tailadmissible",
 418     `:(A->A->bool)->((A->B)->P->bool)->(P->A)->((A->B)->P->B)->bool`);
 419    ("admissible",
 420     `:(B->A->bool)->((B->C)->D->bool)->(D->A)->((B->C)->D->E)->bool`);
 421    ("CASEWISE", `:((A->C)#(B->A->D))list->B->C->D`);
 422    ("vector", `:(A)list->A^N`);
 423    ("dest_auto_define_finite_type_3", `:3->num`);
 424    ("mk_auto_define_finite_type_3", `:num->3`);
 425    ("dest_auto_define_finite_type_2", `:2->num`);
 426    ("mk_auto_define_finite_type_2", `:num->2`);
 427    ("sndcart", `:A^(M,N)finite_sum->A^N`);
 428    ("fstcart", `:A^(M,N)finite_sum->A^M`);
 429    ("pastecart", `:A^M->A^N->A^(M,N)finite_sum`);
 430    ("dest_finite_sum", `:(A,B)finite_sum->num`);
 431    ("mk_finite_sum", `:num->(A,B)finite_sum`); ("lambda", `:(num->A)->A^B`);
 432    ("$", `:B^A->num->B`); ("dest_cart", `:A^B->(B)finite_image->A`);
 433    ("mk_cart", `:((B)finite_image->A)->A^B`);
 434    ("dest_finite_image", `:(A)finite_image->num`);
 435    ("finite_index", `:num->(A)finite_image`);
 436    ("dimindex", `:(A->bool)->num`); ("sum", `:(A->bool)->(A->real)->real`);
 437    ("nsum", `:(A->bool)->(A->num)->num`);
 438    ("iterate", `:(B->B->B)->(A->bool)->(A->B)->B`);
 439    ("support", `:(B->B->B)->(A->B)->(A->bool)->A->bool`);
 440    ("monoidal", `:(A->A->A)->bool`); ("neutral", `:(A->A->A)->A`);
 441    ("..", `:num->num->num->bool`); ("COUNTABLE", `:(A->bool)->bool`);
 442    (">_c", `:(A->bool)->(B->bool)->bool`);
 443    (">=_c", `:(A->bool)->(B->bool)->bool`);
 444    ("=_c", `:(A->bool)->(B->bool)->bool`);
 445    ("<_c", `:(A->bool)->(B->bool)->bool`);
 446    ("<=_c", `:(A->bool)->(B->bool)->bool`);
 447    ("PAIRWISE", `:(A->A->bool)->(A)list->bool`);
 448    ("pairwise", `:(A->A->bool)->(A->bool)->bool`);
 449    ("list_of_set", `:(A->bool)->(A)list`);
 450    ("set_of_list", `:(A)list->A->bool`);
 451    ("CROSS", `:(A->bool)->(B->bool)->A#B->bool`);
 452    ("HAS_SIZE", `:(A->bool)->num->bool`); ("CARD", `:(A->bool)->num`);
 453    ("ITSET", `:(A->B->B)->(A->bool)->B->B`);
 454    ("FINREC", `:(A->B->B)->B->(A->bool)->B->num->bool`);
 455    ("REST", `:(A->bool)->A->bool`); ("CHOICE", `:(A->bool)->A`);
 456    ("BIJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
 457    ("SURJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
 458    ("INJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
 459    ("IMAGE", `:(A->B)->(A->bool)->B->bool`);
 460    ("INFINITE", `:(A->bool)->bool`); ("FINITE", `:(A->bool)->bool`);
 461    ("SING", `:(A->bool)->bool`); ("DISJOINT", `:(A->bool)->(A->bool)->bool`);
 462    ("PSUBSET", `:(A->bool)->(A->bool)->bool`);
 463    ("SUBSET", `:(A->bool)->(A->bool)->bool`);
 464    ("DELETE", `:(A->bool)->A->A->bool`);
 465    ("DIFF", `:(A->bool)->(A->bool)->A->bool`);
 466    ("INTERS", `:((A->bool)->bool)->A->bool`);
 467    ("INTER", `:(A->bool)->(A->bool)->A->bool`);
 468    ("UNIONS", `:((A->bool)->bool)->A->bool`);
 469    ("UNION", `:(A->bool)->(A->bool)->A->bool`); ("UNIV", `:A->bool`);
 470    ("INSERT", `:A->(A->bool)->A->bool`); ("EMPTY", `:A->bool`);
 471    ("SETSPEC", `:A->bool->A->bool`); ("GSPEC", `:(A->bool)->A->bool`);
 472    ("IN", `:A->(A->bool)->bool`); ("num_gcd", `:num#num->num`);
 473    ("num_coprime", `:num#num->bool`); ("num_mod", `:num->num->num->bool`);
 474    ("num_divides", `:num->num->bool`); ("num_of_int", `:int->num`);
 475    ("int_gcd", `:int#int->int`); ("int_coprime", `:int#int->bool`);
 476    ("int_mod", `:int->int->int->bool`); ("int_divides", `:int->int->bool`);
 477    ("real_mod", `:real->real->real->bool`);
 478    ("==", `:A->A->(A->A->bool)->bool`); ("rem", `:int->int->int`);
 479    ("div", `:int->int->int`); ("int_pow", `:int->num->int`);
 480    ("int_min", `:int->int->int`); ("int_max", `:int->int->int`);
 481    ("int_abs", `:int->int`); ("int_mul", `:int->int->int`);
 482    ("int_sub", `:int->int->int`); ("int_add", `:int->int->int`);
 483    ("int_neg", `:int->int`); ("int_of_num", `:num->int`);
 484    ("int_gt", `:int->int->bool`); ("int_ge", `:int->int->bool`);
 485    ("int_lt", `:int->int->bool`); ("int_le", `:int->int->bool`);
 486    ("real_of_int", `:int->real`); ("int_of_real", `:real->int`);
 487    ("is_int", `:real->bool`); ("DECIMAL", `:num->num->real`);
 488    ("real_min", `:real->real->real`); ("real_max", `:real->real->real`);
 489    ("real_div", `:real->real->real`); ("real_pow", `:real->num->real`);
 490    ("real_abs", `:real->real`); ("real_gt", `:real->real->bool`);
 491    ("real_ge", `:real->real->bool`); ("real_lt", `:real->real->bool`);
 492    ("real_sub", `:real->real->real`); ("real_inv", `:real->real`);
 493    ("real_le", `:real->real->bool`); ("real_mul", `:real->real->real`);
 494    ("real_add", `:real->real->real`); ("real_neg", `:real->real`);
 495    ("real_of_num", `:num->real`); ("dest_real", `:real->hreal#hreal->bool`);
 496    ("mk_real", `:(hreal#hreal->bool)->real`);
 497    ("treal_eq", `:hreal#hreal->hreal#hreal->bool`);
 498    ("treal_inv", `:hreal#hreal->hreal#hreal`);
 499    ("treal_le", `:hreal#hreal->hreal#hreal->bool`);
 500    ("treal_mul", `:hreal#hreal->hreal#hreal->hreal#hreal`);
 501    ("treal_add", `:hreal#hreal->hreal#hreal->hreal#hreal`);
 502    ("treal_neg", `:hreal#hreal->hreal#hreal`);
 503    ("treal_of_num", `:num->hreal#hreal`); ("hreal_inv", `:hreal->hreal`);
 504    ("hreal_le", `:hreal->hreal->bool`);
 505    ("hreal_mul", `:hreal->hreal->hreal`);
 506    ("hreal_add", `:hreal->hreal->hreal`); ("hreal_of_num", `:num->hreal`);
 507    ("dest_hreal", `:hreal->nadd->bool`);
 508    ("mk_hreal", `:(nadd->bool)->hreal`); ("nadd_inv", `:nadd->nadd`);
 509    ("nadd_rinv", `:nadd->num->num`); ("nadd_mul", `:nadd->nadd->nadd`);
 510    ("nadd_add", `:nadd->nadd->nadd`); ("nadd_le", `:nadd->nadd->bool`);
 511    ("nadd_of_num", `:num->nadd`); ("nadd_eq", `:nadd->nadd->bool`);
 512    ("dest_nadd", `:nadd->num->num`); ("mk_nadd", `:(num->num)->nadd`);
 513    ("is_nadd", `:(num->num)->bool`); ("dist", `:num#num->num`);
 514    ("ASCII", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
 515    ("_16756", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
 516    ("_dest_char", `:char->(bool#bool#bool#bool#bool#bool#bool#bool)recspace`);
 517    ("_mk_char", `:(bool#bool#bool#bool#bool#bool#bool#bool)recspace->char`);
 518    ("ZIP", `:(A)list->(B)list->(A#B)list`);
 519    ("ITLIST2", `:(A->B->C->C)->(A)list->(B)list->C->C`);
 520    ("ASSOC", `:A->(A#B)list->B`); ("FILTER", `:(A->bool)->(A)list->(A)list`);
 521    ("EL", `:num->(A)list->A`);
 522    ("MAP2", `:(A->B->C)->(A)list->(B)list->(C)list`);
 523    ("ALL2", `:(A->B->bool)->(A)list->(B)list->bool`);
 524    ("MEM", `:A->(A)list->bool`); ("ITLIST", `:(A->B->B)->(A)list->B->B`);
 525    ("EX", `:(A->bool)->(A)list->bool`); ("ALL", `:(A->bool)->(A)list->bool`);
 526    ("NULL", `:(A)list->bool`); ("REPLICATE", `:num->A->(A)list`);
 527    ("LAST", `:(A)list->A`); ("MAP", `:(A->B)->(A)list->(B)list`);
 528    ("LENGTH", `:(A)list->num`); ("REVERSE", `:(A)list->(A)list`);
 529    ("APPEND", `:(A)list->(A)list->(A)list`); ("TL", `:(A)list->(A)list`);
 530    ("HD", `:(A)list->A`); ("ISO", `:(A->B)->(B->A)->bool`);
 531    ("CONS", `:A->(A)list->(A)list`); ("NIL", `:(A)list`);
 532    ("_dest_list", `:(A)list->(A)recspace`);
 533    ("_mk_list", `:(A)recspace->(A)list`); ("SOME", `:A->(A)option`);
 534    ("NONE", `:(A)option`); ("_dest_option", `:(A)option->(A)recspace`);
 535    ("_mk_option", `:(A)recspace->(A)option`); ("OUTR", `:A+B->B`);
 536    ("OUTL", `:A+B->A`); ("INR", `:B->A+B`); ("INL", `:A->A+B`);
 537    ("_dest_sum", `:A+B->(A#B)recspace`); ("_mk_sum", `:(A#B)recspace->A+B`);
 538    ("FNIL", `:num->A`); ("FCONS", `:A->(num->A)->num->A`);
 539    ("CONSTR", `:num->A->(num->(A)recspace)->(A)recspace`);
 540    ("BOTTOM", `:(A)recspace`); ("_dest_rec", `:(A)recspace->num->A->bool`);
 541    ("_mk_rec", `:(num->A->bool)->(A)recspace`);
 542    ("ZRECSPACE", `:(num->A->bool)->bool`); ("ZBOT", `:num->A->bool`);
 543    ("ZCONSTR", `:num->A->(num->num->A->bool)->num->A->bool`);
 544    ("INJP", `:(num->A->bool)->(num->A->bool)->num->A->bool`);
 545    ("INJF", `:(num->num->A->bool)->num->A->bool`);
 546    ("INJA", `:A->num->A->bool`); ("INJN", `:num->num->A->bool`);
 547    ("NUMRIGHT", `:num->num`); ("NUMLEFT", `:num->bool`);
 548    ("NUMSUM", `:bool->num->num`); ("NUMSND", `:num->num`);
 549    ("NUMFST", `:num->num`); ("NUMPAIR", `:num->num->num`);
 550    ("MEASURE", `:(A->num)->A->A->bool`); ("WF", `:(A->A->bool)->bool`);
 551    ("minimal", `:(num->bool)->num`); ("MIN", `:num->num->num`);
 552    ("MAX", `:num->num->num`); ("MOD", `:num->num->num`);
 553    ("DIV", `:num->num->num`); ("FACT", `:num->num`); ("-", `:num->num->num`);
 554    ("ODD", `:num->bool`); ("EVEN", `:num->bool`); (">", `:num->num->bool`);
 555    (">=", `:num->num->bool`); ("<", `:num->num->bool`);
 556    ("<=", `:num->num->bool`); ("EXP", `:num->num->num`);
 557    ("*", `:num->num->num`); ("BIT1", `:num->num`); ("BIT0", `:num->num`);
 558    ("+", `:num->num->num`); ("PRE", `:num->num`); ("NUMERAL", `:num->num`);
 559    ("SUC", `:num->num`); ("_0", `:num`); ("dest_num", `:num->ind`);
 560    ("mk_num", `:ind->num`); ("NUM_REP", `:ind->bool`); ("IND_0", `:ind`);
 561    ("IND_SUC", `:ind->ind`); ("ONTO", `:(A->B)->bool`);
 562    ("ONE_ONE", `:(A->B)->bool`); ("PASSOC", `:((A#B)#C->D)->A#B#C->D`);
 563    ("UNCURRY", `:(A->B->C)->A#B->C`); ("CURRY", `:(A#B->C)->A->B->C`);
 564    ("SND", `:A#B->B`); ("FST", `:A#B->A`); (",", `:A->B->A#B`);
 565    ("REP_prod", `:A#B->A->B->bool`); ("ABS_prod", `:(A->B->bool)->A#B`);
 566    ("mk_pair", `:A->B->A->B->bool`); ("_FUNCTION", `:(A->B->bool)->A->B`);
 567    ("_MATCH", `:A->(A->B->bool)->B`);
 568    ("_GUARDED_PATTERN", `:bool->bool->bool->bool`);
 569    ("_UNGUARDED_PATTERN", `:bool->bool->bool`);
 570    ("_SEQPATTERN", `:(A->B->bool)->(A->B->bool)->A->B->bool`);
 571    ("GEQ", `:A->A->bool`); ("GABS", `:(A->bool)->A`); ("LET_END", `:A->A`);
 572    ("LET", `:(A->B)->A->B`); ("one", `:1`); ("one_REP", `:1->bool`);
 573    ("one_ABS", `:bool->1`); ("I", `:A->A`); ("o", `:(B->C)->(A->B)->A->C`);
 574    ("COND", `:bool->A->A->A`); ("@", `:(A->bool)->A`);
 575    ("_FALSITY_", `:bool`); ("?!", `:(A->bool)->bool`); ("~", `:bool->bool`);
 576    ("F", `:bool`); ("\\/", `:bool->bool->bool`); ("?", `:(A->bool)->bool`);
 577    ("!", `:(A->bool)->bool`); ("==>", `:bool->bool->bool`);
 578    ("/\\", `:bool->bool->bool`); ("T", `:bool`); ("=", `:A->A->bool`)];;
 579
 580 end;;
 581
 582
 583 module Snapshot_v220_7_31_2009 : Snapshot_type = struct
 584
 585   let the_constants =
 586   [("SDIFF", `:(A->bool)->(A->bool)->A->bool`);
 587    ("vol_ball_wedge", `:real^3->real^3->real^3->real^3->real->real`);
 588    ("vol_rect", `:real^A->real^B->real`);
 589    ("vol_conv", `:real^A->real^A->real^A->real^A->real`);
 590    ("vol_conic_cap_wedge",
 591     `:real^3->real^3->real^3->real^3->real->real->real`);
 592    ("vol_frustt_wedge", `:real^3->real^3->real^3->real^3->real->real->real`);
 593    ("vol_solid_triangle", `:real^A->real^A->real^A->real^A->real->real`);
 594    ("primitive", `:(real^3->bool)->bool`);
 595    ("circular_cone", `:(real^3->bool)->bool`);
 596    ("c_cone", `:real^3#real^3#real->real^3->bool`);
 597    ("sphere", `:(real^3->bool)->bool`);
 598    ("rect", `:real^3->real^3->real^3->bool`);
 599    ("solid_triangle", `:real^A->(real^A->bool)->real->real^A->bool`);
 600    ("cone0", `:real^A->(real^A->bool)->real^A->bool`);
 601    ("cone", `:real^A->(real^A->bool)->real^A->bool`);
 602    ("dihV", `:real^A->real^A->real^A->real^A->real`);
 603    ("opposite", `:real^N->real^N->(real^N->bool)->bool`);
 604    ("wedge", `:real^3->real^3->real^3->real^3->real^3->bool`);
 605    ("azim", `:real^3->real^3->real^3->real^3->real`);
 606    ("arcV", `:real^A->real^A->real^A->real`);
 607    ("orthonormal", `:real^3->real^3->real^3->bool`);
 608    ("conic_cap", `:real^A->real^A->real->real->real^A->bool`);
 609    ("ellipsoid", `:real^3->real->real^3->bool`);
 610    ("normball", `:real^A->real->real^A->bool`);
 611    ("scale", `:real^3->real^3->real^3`);
 612    ("frustt", `:real^A->real^A->real->real->real^A->bool`);
 613    ("frustum", `:real^N->real^N->real->real->real->real^N->bool`);
 614    ("rcone_eq", `:real^A->real^A->real->real^A->bool`);
 615    ("rcone_ge", `:real^A->real^A->real->real^A->bool`);
 616    ("rcone_gt", `:real^A->real^A->real->real^A->bool`);
 617    ("rconesgn", `:(real->real->bool)->real^A->real^A->real->real^A->bool`);
 618    ("delta_x", `:real->real->real->real->real->real->real`);
 619    ("conv0", `:(real^A->bool)->real^A->bool`);
 620    ("aff_le", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 621    ("aff_lt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 622    ("aff_ge", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 623    ("aff_gt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
 624    ("sgn_le", `:real->bool`); ("sgn_lt", `:real->bool`);
 625    ("sgn_ge", `:real->bool`); ("sgn_gt", `:real->bool`);
 626    ("affsign", `:(real->bool)->(real^A->bool)->(real^A->bool)->real^A->bool`);
 627    ("lin_combo", `:(real^N->bool)->(real^N->real)->real^N`);
 628    ("pad2d3d", `:real^2->real^3`); ("plane", `:(real^A->bool)->bool`);
 629    ("slice", `:num->real->(real^A->bool)->real^B->bool`);
 630    ("pushin", `:num->B->B^A->B^C`); ("dropout", `:num->real^N->real^M`);
 631    ("real_measure", `:(real->bool)->real`);
 632    ("real_measurable", `:(real->bool)->bool`);
 633    ("has_real_measure", `:(real->bool)->real->bool`);
 634    ("absolutely_real_integrable_on", `:(real->real)->(real->bool)->bool`);
 635    ("real_negligible", `:(real->bool)->bool`);
 636    ("real_integral", `:(real->bool)->(real->real)->real`);
 637    ("real_integrable_on", `:(real->real)->(real->bool)->bool`);
 638    ("has_real_integral", `:(real->real)->real->(real->bool)->bool`);
 639    ("closed_real_interval", `:(real#real)list->real->bool`);
 640    ("open_real_interval", `:real#real->real->bool`);
 641    ("is_realinterval", `:(real->bool)->bool`);
 642    ("real_differentiable_on", `:(real->real)->(real->bool)->bool`);
 643    ("higher_real_derivative", `:num->(real->real)->real->real`);
 644    ("real_derivative", `:(real->real)->real->real`);
 645    ("real_differentiable", `:(real->real)->(real)net->bool`);
 646    ("has_real_derivative", `:(real->real)->real->(real)net->bool`);
 647    ("real_continuous_on", `:(real->real)->(real->bool)->bool`);
 648    ("real_continuous", `:(A->real)->(A)net->bool`);
 649    ("at_neginfinity", `:(real)net`); ("at_posinfinity", `:(real)net`);
 650    ("atreal", `:real->(real)net`);
 651    ("real_summable", `:(num->bool)->(num->real)->bool`);
 652    ("real_infsum", `:(num->bool)->(num->real)->real`);
 653    ("real_sums", `:(num->real)->real->(num->bool)->bool`);
 654    ("--->", `:(A->real)->real->(A)net->bool`);
 655    ("real_compact", `:(real->bool)->bool`);
 656    ("real_bounded", `:(real->bool)->bool`);
 657    ("euclideanreal", `:(real)topology`);
 658    ("real_closed", `:(real->bool)->bool`);
 659    ("real_open", `:(real->bool)->bool`);
 660    ("measure", `:(real^A->bool)->real`);
 661    ("measurable", `:(real^A->bool)->bool`);
 662    ("has_measure", `:(real^A->bool)->real->bool`);
 663    ("*_c", `:(A->bool)->(B->bool)->A#B->bool`);
 664    ("+_c", `:(A->bool)->(B->bool)->A+B->bool`);
 665    ("ordinal", `:(A#A->bool)->bool`);
 666    ("linseg", `:(A#A->bool)->A->A#A->bool`);
 667    ("inseg", `:(A#A->bool)->(A#A->bool)->bool`);
 668    ("woset", `:(A#A->bool)->bool`);
 669    ("chain", `:(A#A->bool)->(A->bool)->bool`);
 670    ("poset", `:(A#A->bool)->bool`); ("fl", `:(A#A->bool)->A->bool`);
 671    ("less", `:(A#A->bool)->A#A->bool`);
 672    ("angle", `:real^A#real^A#real^A->real`);
 673    ("vector_angle", `:real^A->real^A->real`); ("acs", `:real->real`);
 674    ("asn", `:real->real`); ("cacs", `:real^2->real^2`);
 675    ("casn", `:real^2->real^2`); ("atn", `:real->real`);
 676    ("catn", `:real^2->real^2`); ("unwinding", `:real^2->real^2`);
 677    ("cpow", `:real^2->real^2->real^2`); ("clog", `:real^2->real^2`);
 678    ("tan", `:real->real`); ("ctan", `:real^2->real^2`);
 679    ("rotate2d", `:real->real^2->real^2`); ("Arg", `:real^2->real`);
 680    ("pi", `:real`); ("log", `:real->real`); ("cos", `:real->real`);
 681    ("sin", `:real->real`); ("exp", `:real->real`);
 682    ("csin", `:real^2->real^2`); ("ccos", `:real^2->real^2`);
 683    ("cexp", `:real^2->real^2`);
 684    ("analytic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
 685    ("holomorphic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
 686    ("higher_complex_derivative", `:num->(real^2->real^2)->real^2->real^2`);
 687    ("complex_derivative", `:(real^2->real^2)->real^2->real^2`);
 688    ("complex_differentiable", `:(real^2->real^2)->(real^2)net->bool`);
 689    ("has_complex_derivative", `:(real^2->real^2)->real^2->(real^2)net->bool`);
 690    ("cproduct", `:(A->bool)->(A->real^2)->real^2`);
 691    ("real", `:real^2->bool`); ("csqrt", `:real^2->real^2`);
 692    ("cnj", `:real^2->real^2`); ("complex_pow", `:real^2->num->real^2`);
 693    ("complex_div", `:real^2->real^2->real^2`);
 694    ("complex_inv", `:real^2->real^2`);
 695    ("complex_mul", `:real^2->real^2->real^2`); ("ii", `:real^2`);
 696    ("Cx", `:real->real^2`); ("complex", `:real#real->real^2`);
 697    ("Im", `:real^2->real`); ("Re", `:real^2->real`);
 698    ("absolutely_integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 699    ("negligible", `:(real^A->bool)->bool`);
 700    ("indicator", `:(real^M->bool)->real^M->real^1`);
 701    ("division_points",
 702     `:(real^N->bool)->((real^N->bool)->bool)->num#real->bool`);
 703    ("lifted", `:(A->A->B)->(A)option->(A)option->(B)option`);
 704    ("operative", `:(A->A->A)->((real^N->bool)->A)->bool`);
 705    ("integral", `:(real^A->bool)->(real^A->real^B)->real^B`);
 706    ("integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 707    ("has_integral", `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
 708    ("has_integral_compact_interval",
 709     `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
 710    ("fine", `:(A->B->bool)->(A#(B->bool)->bool)->bool`);
 711    ("tagged_division_of",
 712     `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
 713    ("tagged_partial_division_of",
 714     `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
 715    ("division_of", `:((real^A->bool)->bool)->(real^A->bool)->bool`);
 716    ("gauge", `:(real^A->real^A->bool)->bool`);
 717    ("content", `:(real^M->bool)->real`);
 718    ("interval_lowerbound", `:(real^M->bool)->real^M`);
 719    ("interval_upperbound", `:(real^M->bool)->real^M`);
 720    ("vector_derivative", `:(real^1->real^N)->(real^1)net->real^N`);
 721    ("has_vector_derivative", `:(real^1->real^A)->real^A->(real^1)net->bool`);
 722    ("jacobian", `:(real^A->real^B)->(real^A)net->real^A^B`);
 723    ("frechet_derivative", `:(real^A->real^B)->(real^A)net->real^A->real^B`);
 724    ("differentiable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 725    ("differentiable", `:(real^B->real^A)->(real^B)net->bool`);
 726    ("has_derivative",
 727     `:(real^B->real^A)->(real^B->real^A)->(real^B)net->bool`);
 728    ("interval_bij", `:real^N#real^N->real^N#real^N->real^N->real^N`);
 729    ("retract_of", `:(real^A->bool)->(real^A->bool)->bool`);
 730    ("retraction", `:(real^N->bool)#(real^N->bool)->(real^N->real^N)->bool`);
 731    ("reduced", `:((num->num)->num->num)->num->(num->num)->num`);
 732    ("ksimplex", `:num->num->((num->num)->bool)->bool`);
 733    ("kle", `:num->(num->num)->(num->num)->bool`);
 734    ("path_connected", `:(real^A->bool)->bool`);
 735    ("path_component", `:(real^A->bool)->real^A->real^A->bool`);
 736    ("linepath", `:real^A#real^A->real^1->real^A`);
 737    ("shiftpath", `:real^1->(real^1->real^N)->real^1->real^N`);
 738    ("arc", `:(real^1->real^N)->bool`);
 739    ("simple_path", `:(real^1->real^N)->bool`);
 740    ("++", `:(real^1->A)->(real^1->A)->real^1->A`);
 741    ("reversepath", `:(real^1->real^N)->real^1->real^N`);
 742    ("path_image", `:(real^1->real^N)->real^N->bool`);
 743    ("pathfinish", `:(real^1->real^N)->real^N`);
 744    ("pathstart", `:(real^1->real^N)->real^N`);
 745    ("path", `:(real^1->real^N)->bool`);
 746    ("extreme_point_of", `:real^A->(real^A->bool)->bool`);
 747    ("face_of", `:(real^A->bool)->(real^A->bool)->bool`);
 748    ("relative_interior", `:(real^A->bool)->real^A->bool`);
 749    ("starlike", `:(real^A->bool)->bool`);
 750    ("epigraph",
 751     `:(real^N->bool)->(real^N->real)->real^(N,1)finite_sum->bool`);
 752    ("convex_on", `:(real^A->real)->(real^A->bool)->bool`);
 753    ("coplanar", `:(real^A->bool)->bool`);
 754    ("affine_dependent", `:(real^N->bool)->bool`);
 755    ("conic", `:(real^A->bool)->bool`); ("convex", `:(real^A->bool)->bool`);
 756    ("affine", `:(real^A->bool)->bool`);
 757    ("closest_point", `:(real^A->bool)->real^A->real^A`);
 758    ("from", `:num->num->bool`);
 759    ("summable", `:(num->bool)->(num->real^A)->bool`);
 760    ("infsum", `:(num->bool)->(num->real^A)->real^A`);
 761    ("sums", `:(num->real^A)->real^A->(num->bool)->bool`);
 762    ("homeomorphic", `:(real^A->bool)->(real^B->bool)->bool`);
 763    ("homeomorphism",
 764     `:(real^B->bool)#(real^A->bool)->(real^B->real^A)#(real^A->real^B)->bool`);
 765    ("open_segment", `:real^A#real^A->real^A->bool`);
 766    ("closed_segment", `:(real^A#real^A)list->real^A->bool`);
 767    ("is_interval", `:(real^N->bool)->bool`);
 768    ("closed_interval", `:(real^N#real^N)list->real^N->bool`);
 769    ("open_interval", `:real^N#real^N->real^N->bool`);
 770    ("diameter", `:(real^A->bool)->real`);
 771    ("connected_component", `:(real^A->bool)->real^A->real^A->bool`);
 772    ("uniformly_continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 773    ("continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
 774    ("continuous", `:(B->real^A)->(B)net->bool`);
 775    ("complete", `:(real^N->bool)->bool`); ("cauchy", `:(num->real^N)->bool`);
 776    ("compact", `:(real^N->bool)->bool`);
 777    ("bounded", `:(real^N->bool)->bool`); ("netlimit", `:(A)net->A`);
 778    ("lim", `:(A)net->(A->real^B)->real^B`);
 779    ("-->", `:(B->real^A)->real^A->(B)net->bool`);
 780    ("eventually", `:(A->bool)->(A)net->bool`);
 781    ("trivial_limit", `:(A)net->bool`);
 782    ("in_direction", `:real^A->real^A->(real^A)net`);
 783    ("within", `:(A)net->(A->bool)->(A)net`); ("sequentially", `:(num)net`);
 784    ("at_infinity", `:(real^A)net`); ("at", `:real^A->(real^A)net`);
 785    ("netord", `:(A)net->A->A->bool`); ("mk_net", `:(A->A->bool)->(A)net`);
 786    ("frontier", `:(real^A->bool)->real^A->bool`);
 787    ("closure", `:(real^A->bool)->real^A->bool`);
 788    ("interior", `:(real^A->bool)->real^A->bool`);
 789    ("limit_point_of", `:real^A->(real^A->bool)->bool`);
 790    ("connected", `:(real^A->bool)->bool`);
 791    ("cball", `:real^A#real->real^A->bool`);
 792    ("ball", `:real^A#real->real^A->bool`);
 793    ("euclidean", `:(real^A)topology`); ("closed", `:(real^N->bool)->bool`);
 794    ("open", `:(real^A->bool)->bool`);
 795    ("subtopology", `:(A)topology->(A->bool)->(A)topology`);
 796    ("closed_in", `:(A)topology->(A->bool)->bool`);
 797    ("topspace", `:(A)topology->A->bool`);
 798    ("open_in", `:(A)topology->(A->bool)->bool`);
 799    ("topology", `:((A->bool)->bool)->(A)topology`);
 800    ("istopology", `:((A->bool)->bool)->bool`);
 801    ("ITER", `:num->(A->A)->A->A`); ("frac", `:real->real`);
 802    ("floor", `:real->real`); ("integer", `:real->bool`);
 803    ("cross", `:real^3->real^3->real^3`);
 804    ("rotoinversion_matrix", `:real^A^A->bool`);
 805    ("rotation_matrix", `:real^A^A->bool`);
 806    ("orthogonal_matrix", `:real^N^N->bool`);
 807    ("orthogonal_transformation", `:(real^N->real^N)->bool`);
 808    ("det", `:real^N^N->real`); ("trace", `:real^N^N->real`);
 809    ("product", `:(A->bool)->(A->real)->real`); ("sign", `:(A->A)->real`);
 810    ("evenperm", `:(A->A)->bool`); ("permutation", `:(A->A)->bool`);
 811    ("swapseq", `:num->(A->A)->bool`); ("swap", `:A#A->A->A`);
 812    ("inverse", `:(B->A)->A->B`); ("permutes", `:(A->A)->(A->bool)->bool`);
 813    ("midpoint", `:real^A#real^A->real^A`);
 814    ("between", `:real^A->real^A#real^A->bool`);
 815    ("collinear", `:(real^A->bool)->bool`); ("infnorm", `:real^N->real`);
 816    ("rank", `:real^M^N->num`); ("columnvector", `:real^N->real^1^N`);
 817    ("rowvector", `:real^N->real^N^1`); ("dim", `:(real^A->bool)->num`);
 818    ("independent", `:(real^A->bool)->bool`);
 819    ("dependent", `:(real^A->bool)->bool`);
 820    ("span", `:(real^A->bool)->real^A->bool`);
 821    ("subspace", `:(real^A->bool)->bool`); ("drop", `:real^1->real`);
 822    ("lift", `:real->real^1`); ("onorm", `:(real^M->real^N)->real`);
 823    ("matrix", `:(real^M->real^N)->real^M^N`);
 824    ("matrix_inv", `:real^N^M->real^M^N`); ("invertible", `:real^N^M->bool`);
 825    ("columns", `:real^N^M->real^M->bool`);
 826    ("rows", `:real^N^M->real^N->bool`); ("column", `:num->real^N^M->real^M`);
 827    ("row", `:num->real^N^M->real^N`); ("transp", `:real^N^M->real^M^N`);
 828    ("mat", `:num->real^N^M`);
 829    ("vector_matrix_mul", `:real^M->real^N^M->real^N`);
 830    ("matrix_vector_mul", `:real^N^M->real^N->real^M`);
 831    ("matrix_mul", `:real^N^M->real^P^N->real^P^M`);
 832    ("matrix_sub", `:real^N^M->real^N^M->real^N^M`);
 833    ("matrix_add", `:real^N^M->real^N^M->real^N^M`);
 834    ("matrix_neg", `:real^N^M->real^N^M`);
 835    ("adjoint", `:(real^M->real^N)->real^N->real^M`);
 836    ("bilinear", `:(real^A->real^B->real^C)->bool`);
 837    ("linear", `:(real^M->real^N)->bool`);
 838    ("orthogonal", `:real^A->real^A->bool`); ("basis", `:num->real^A`);
 839    ("vsum", `:(A->bool)->(A->real^N)->real^N`);
 840    ("distance", `:real^A#real^A->real`); ("vector_norm", `:real^A->real`);
 841    ("dot", `:real^N->real^N->real`); ("vec", `:num->real^N`);
 842    ("%", `:real->real^N->real^N`); ("vector_neg", `:real^N->real^N`);
 843    ("vector_sub", `:real^N->real^N->real^N`);
 844    ("vector_add", `:real^N->real^N->real^N`); ("sqrt", `:real->real`);
 845    ("hull", `:((A->bool)->bool)->(A->bool)->A->bool`);
 846    ("inf", `:(real->bool)->real`); ("sup", `:(real->bool)->real`);
 847    ("superadmissible",
 848     `:(A->A->bool)->((A->C)->B->bool)->(B->A)->((A->C)->B->C)->bool`);
 849    ("tailadmissible",
 850     `:(A->A->bool)->((A->B)->P->bool)->(P->A)->((A->B)->P->B)->bool`);
 851    ("admissible",
 852     `:(B->A->bool)->((B->C)->D->bool)->(D->A)->((B->C)->D->E)->bool`);
 853    ("CASEWISE", `:((A->C)#(B->A->D))list->B->C->D`);
 854    ("vector", `:(A)list->A^N`);
 855    ("dest_auto_define_finite_type_3", `:3->num`);
 856    ("mk_auto_define_finite_type_3", `:num->3`);
 857    ("dest_auto_define_finite_type_2", `:2->num`);
 858    ("mk_auto_define_finite_type_2", `:num->2`);
 859    ("sndcart", `:A^(M,N)finite_sum->A^N`);
 860    ("fstcart", `:A^(M,N)finite_sum->A^M`);
 861    ("pastecart", `:A^M->A^N->A^(M,N)finite_sum`);
 862    ("dest_finite_sum", `:(A,B)finite_sum->num`);
 863    ("mk_finite_sum", `:num->(A,B)finite_sum`); ("lambda", `:(num->A)->A^B`);
 864    ("$", `:B^A->num->B`); ("dest_cart", `:A^B->(B)finite_image->A`);
 865    ("mk_cart", `:((B)finite_image->A)->A^B`);
 866    ("dest_finite_image", `:(A)finite_image->num`);
 867    ("finite_index", `:num->(A)finite_image`);
 868    ("dimindex", `:(A->bool)->num`); ("sum", `:(A->bool)->(A->real)->real`);
 869    ("nsum", `:(A->bool)->(A->num)->num`);
 870    ("iterate", `:(B->B->B)->(A->bool)->(A->B)->B`);
 871    ("support", `:(B->B->B)->(A->B)->(A->bool)->A->bool`);
 872    ("monoidal", `:(A->A->A)->bool`); ("neutral", `:(A->A->A)->A`);
 873    ("..", `:num->num->num->bool`); ("COUNTABLE", `:(A->bool)->bool`);
 874    (">_c", `:(A->bool)->(B->bool)->bool`);
 875    (">=_c", `:(A->bool)->(B->bool)->bool`);
 876    ("=_c", `:(A->bool)->(B->bool)->bool`);
 877    ("<_c", `:(A->bool)->(B->bool)->bool`);
 878    ("<=_c", `:(A->bool)->(B->bool)->bool`);
 879    ("PAIRWISE", `:(A->A->bool)->(A)list->bool`);
 880    ("pairwise", `:(A->A->bool)->(A->bool)->bool`);
 881    ("list_of_set", `:(A->bool)->(A)list`);
 882    ("set_of_list", `:(A)list->A->bool`);
 883    ("CROSS", `:(A->bool)->(B->bool)->A#B->bool`);
 884    ("HAS_SIZE", `:(A->bool)->num->bool`); ("CARD", `:(A->bool)->num`);
 885    ("ITSET", `:(A->B->B)->(A->bool)->B->B`);
 886    ("FINREC", `:(A->B->B)->B->(A->bool)->B->num->bool`);
 887    ("REST", `:(A->bool)->A->bool`); ("CHOICE", `:(A->bool)->A`);
 888    ("BIJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
 889    ("SURJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
 890    ("INJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
 891    ("IMAGE", `:(A->B)->(A->bool)->B->bool`);
 892    ("INFINITE", `:(A->bool)->bool`); ("FINITE", `:(A->bool)->bool`);
 893    ("SING", `:(A->bool)->bool`); ("DISJOINT", `:(A->bool)->(A->bool)->bool`);
 894    ("PSUBSET", `:(A->bool)->(A->bool)->bool`);
 895    ("SUBSET", `:(A->bool)->(A->bool)->bool`);
 896    ("DELETE", `:(A->bool)->A->A->bool`);
 897    ("DIFF", `:(A->bool)->(A->bool)->A->bool`);
 898    ("INTERS", `:((A->bool)->bool)->A->bool`);
 899    ("INTER", `:(A->bool)->(A->bool)->A->bool`);
 900    ("UNIONS", `:((A->bool)->bool)->A->bool`);
 901    ("UNION", `:(A->bool)->(A->bool)->A->bool`); ("UNIV", `:A->bool`);
 902    ("INSERT", `:A->(A->bool)->A->bool`); ("EMPTY", `:A->bool`);
 903    ("SETSPEC", `:A->bool->A->bool`); ("GSPEC", `:(A->bool)->A->bool`);
 904    ("IN", `:A->(A->bool)->bool`); ("num_gcd", `:num#num->num`);
 905    ("num_coprime", `:num#num->bool`); ("num_mod", `:num->num->num->bool`);
 906    ("num_divides", `:num->num->bool`); ("num_of_int", `:int->num`);
 907    ("int_gcd", `:int#int->int`); ("int_coprime", `:int#int->bool`);
 908    ("int_mod", `:int->int->int->bool`); ("int_divides", `:int->int->bool`);
 909    ("real_mod", `:real->real->real->bool`);
 910    ("==", `:A->A->(A->A->bool)->bool`); ("rem", `:int->int->int`);
 911    ("div", `:int->int->int`); ("int_pow", `:int->num->int`);
 912    ("int_min", `:int->int->int`); ("int_max", `:int->int->int`);
 913    ("int_abs", `:int->int`); ("int_mul", `:int->int->int`);
 914    ("int_sub", `:int->int->int`); ("int_add", `:int->int->int`);
 915    ("int_neg", `:int->int`); ("int_of_num", `:num->int`);
 916    ("int_gt", `:int->int->bool`); ("int_ge", `:int->int->bool`);
 917    ("int_lt", `:int->int->bool`); ("int_le", `:int->int->bool`);
 918    ("real_of_int", `:int->real`); ("int_of_real", `:real->int`);
 919    ("is_int", `:real->bool`); ("DECIMAL", `:num->num->real`);
 920    ("real_min", `:real->real->real`); ("real_max", `:real->real->real`);
 921    ("real_div", `:real->real->real`); ("real_pow", `:real->num->real`);
 922    ("real_abs", `:real->real`); ("real_gt", `:real->real->bool`);
 923    ("real_ge", `:real->real->bool`); ("real_lt", `:real->real->bool`);
 924    ("real_sub", `:real->real->real`); ("real_inv", `:real->real`);
 925    ("real_le", `:real->real->bool`); ("real_mul", `:real->real->real`);
 926    ("real_add", `:real->real->real`); ("real_neg", `:real->real`);
 927    ("real_of_num", `:num->real`); ("dest_real", `:real->hreal#hreal->bool`);
 928    ("mk_real", `:(hreal#hreal->bool)->real`);
 929    ("treal_eq", `:hreal#hreal->hreal#hreal->bool`);
 930    ("treal_inv", `:hreal#hreal->hreal#hreal`);
 931    ("treal_le", `:hreal#hreal->hreal#hreal->bool`);
 932    ("treal_mul", `:hreal#hreal->hreal#hreal->hreal#hreal`);
 933    ("treal_add", `:hreal#hreal->hreal#hreal->hreal#hreal`);
 934    ("treal_neg", `:hreal#hreal->hreal#hreal`);
 935    ("treal_of_num", `:num->hreal#hreal`); ("hreal_inv", `:hreal->hreal`);
 936    ("hreal_le", `:hreal->hreal->bool`);
 937    ("hreal_mul", `:hreal->hreal->hreal`);
 938    ("hreal_add", `:hreal->hreal->hreal`); ("hreal_of_num", `:num->hreal`);
 939    ("dest_hreal", `:hreal->nadd->bool`);
 940    ("mk_hreal", `:(nadd->bool)->hreal`); ("nadd_inv", `:nadd->nadd`);
 941    ("nadd_rinv", `:nadd->num->num`); ("nadd_mul", `:nadd->nadd->nadd`);
 942    ("nadd_add", `:nadd->nadd->nadd`); ("nadd_le", `:nadd->nadd->bool`);
 943    ("nadd_of_num", `:num->nadd`); ("nadd_eq", `:nadd->nadd->bool`);
 944    ("dest_nadd", `:nadd->num->num`); ("mk_nadd", `:(num->num)->nadd`);
 945    ("is_nadd", `:(num->num)->bool`); ("dist", `:num#num->num`);
 946    ("ASCII", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
 947    ("_16756", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
 948    ("_dest_char", `:char->(bool#bool#bool#bool#bool#bool#bool#bool)recspace`);
 949    ("_mk_char", `:(bool#bool#bool#bool#bool#bool#bool#bool)recspace->char`);
 950    ("ZIP", `:(A)list->(B)list->(A#B)list`);
 951    ("ITLIST2", `:(A->B->C->C)->(A)list->(B)list->C->C`);
 952    ("ASSOC", `:A->(A#B)list->B`); ("FILTER", `:(A->bool)->(A)list->(A)list`);
 953    ("EL", `:num->(A)list->A`);
 954    ("MAP2", `:(A->B->C)->(A)list->(B)list->(C)list`);
 955    ("ALL2", `:(A->B->bool)->(A)list->(B)list->bool`);
 956    ("MEM", `:A->(A)list->bool`); ("ITLIST", `:(A->B->B)->(A)list->B->B`);
 957    ("EX", `:(A->bool)->(A)list->bool`); ("ALL", `:(A->bool)->(A)list->bool`);
 958    ("NULL", `:(A)list->bool`); ("REPLICATE", `:num->A->(A)list`);
 959    ("LAST", `:(A)list->A`); ("MAP", `:(A->B)->(A)list->(B)list`);
 960    ("LENGTH", `:(A)list->num`); ("REVERSE", `:(A)list->(A)list`);
 961    ("APPEND", `:(A)list->(A)list->(A)list`); ("TL", `:(A)list->(A)list`);
 962    ("HD", `:(A)list->A`); ("ISO", `:(A->B)->(B->A)->bool`);
 963    ("CONS", `:A->(A)list->(A)list`); ("NIL", `:(A)list`);
 964    ("_dest_list", `:(A)list->(A)recspace`);
 965    ("_mk_list", `:(A)recspace->(A)list`); ("SOME", `:A->(A)option`);
 966    ("NONE", `:(A)option`); ("_dest_option", `:(A)option->(A)recspace`);
 967    ("_mk_option", `:(A)recspace->(A)option`); ("OUTR", `:A+B->B`);
 968    ("OUTL", `:A+B->A`); ("INR", `:B->A+B`); ("INL", `:A->A+B`);
 969    ("_dest_sum", `:A+B->(A#B)recspace`); ("_mk_sum", `:(A#B)recspace->A+B`);
 970    ("FNIL", `:num->A`); ("FCONS", `:A->(num->A)->num->A`);
 971    ("CONSTR", `:num->A->(num->(A)recspace)->(A)recspace`);
 972    ("BOTTOM", `:(A)recspace`); ("_dest_rec", `:(A)recspace->num->A->bool`);
 973    ("_mk_rec", `:(num->A->bool)->(A)recspace`);
 974    ("ZRECSPACE", `:(num->A->bool)->bool`); ("ZBOT", `:num->A->bool`);
 975    ("ZCONSTR", `:num->A->(num->num->A->bool)->num->A->bool`);
 976    ("INJP", `:(num->A->bool)->(num->A->bool)->num->A->bool`);
 977    ("INJF", `:(num->num->A->bool)->num->A->bool`);
 978    ("INJA", `:A->num->A->bool`); ("INJN", `:num->num->A->bool`);
 979    ("NUMRIGHT", `:num->num`); ("NUMLEFT", `:num->bool`);
 980    ("NUMSUM", `:bool->num->num`); ("NUMSND", `:num->num`);
 981    ("NUMFST", `:num->num`); ("NUMPAIR", `:num->num->num`);
 982    ("MEASURE", `:(A->num)->A->A->bool`); ("WF", `:(A->A->bool)->bool`);
 983    ("minimal", `:(num->bool)->num`); ("MIN", `:num->num->num`);
 984    ("MAX", `:num->num->num`); ("MOD", `:num->num->num`);
 985    ("DIV", `:num->num->num`); ("FACT", `:num->num`); ("-", `:num->num->num`);
 986    ("ODD", `:num->bool`); ("EVEN", `:num->bool`); (">", `:num->num->bool`);
 987    (">=", `:num->num->bool`); ("<", `:num->num->bool`);
 988    ("<=", `:num->num->bool`); ("EXP", `:num->num->num`);
 989    ("*", `:num->num->num`); ("BIT1", `:num->num`); ("BIT0", `:num->num`);
 990    ("+", `:num->num->num`); ("PRE", `:num->num`); ("NUMERAL", `:num->num`);
 991    ("SUC", `:num->num`); ("_0", `:num`); ("dest_num", `:num->ind`);
 992    ("mk_num", `:ind->num`); ("NUM_REP", `:ind->bool`); ("IND_0", `:ind`);
 993    ("IND_SUC", `:ind->ind`); ("ONTO", `:(A->B)->bool`);
 994    ("ONE_ONE", `:(A->B)->bool`); ("PASSOC", `:((A#B)#C->D)->A#B#C->D`);
 995    ("UNCURRY", `:(A->B->C)->A#B->C`); ("CURRY", `:(A#B->C)->A->B->C`);
 996    ("SND", `:A#B->B`); ("FST", `:A#B->A`); (",", `:A->B->A#B`);
 997    ("REP_prod", `:A#B->A->B->bool`); ("ABS_prod", `:(A->B->bool)->A#B`);
 998    ("mk_pair", `:A->B->A->B->bool`); ("_FUNCTION", `:(A->B->bool)->A->B`);
 999    ("_MATCH", `:A->(A->B->bool)->B`);
1000    ("_GUARDED_PATTERN", `:bool->bool->bool->bool`);
1001    ("_UNGUARDED_PATTERN", `:bool->bool->bool`);
1002    ("_SEQPATTERN", `:(A->B->bool)->(A->B->bool)->A->B->bool`);
1003    ("GEQ", `:A->A->bool`); ("GABS", `:(A->bool)->A`); ("LET_END", `:A->A`);
1004    ("LET", `:(A->B)->A->B`); ("one", `:1`); ("one_REP", `:1->bool`);
1005    ("one_ABS", `:bool->1`); ("I", `:A->A`); ("o", `:(B->C)->(A->B)->A->C`);
1006    ("COND", `:bool->A->A->A`); ("@", `:(A->bool)->A`);
1007    ("_FALSITY_", `:bool`); ("?!", `:(A->bool)->bool`); ("~", `:bool->bool`);
1008    ("F", `:bool`); ("\\/", `:bool->bool->bool`); ("?", `:(A->bool)->bool`);
1009    ("!", `:(A->bool)->bool`); ("==>", `:bool->bool->bool`);
1010    ("/\\", `:bool->bool->bool`); ("T", `:bool`); ("=", `:A->A->bool`)];;
1011
1012   let the_loaded_files =  ["flyspeck.ml"; "wlog_examples.ml"; "wlog.ml"; "real.ml"; "measure.ml";
1013    "card.ml"; "wo.ml"; "geom.ml"; "transc.ml"; "canal.ml"; "complex.ml";
1014    "integration.ml"; "analysis.ml"; "dimension.ml"; "convex.ml";
1015    "topology.ml"; "iter.ml"; "floor.ml"; "cross.ml"; "determinants.ml";
1016    "products.ml"; "permutations.ml"; "vectors.ml"; "misc.ml"; "database.ml";
1017    "help.ml"; "define.ml"; "cart.ml"; "iter.ml"; "sets.ml"; "int.ml";
1018    "calc_rat.ml"; "real.ml"; "realarith.ml"; "calc_int.ml"; "realax.ml";
1019    "list.ml"; "ind-types.ml"; "grobner.ml"; "normalizer.ml"; "calc_num.ml";
1020    "wf.ml"; "arith.ml"; "num.ml"; "pair.ml"; "recursion.ml"; "quot.ml";
1021    "meson.ml"; "canon.ml"; "trivia.ml"; "class.ml"; "ind-defs.ml";
1022    "theorems.ml"; "simp.ml"; "itab.ml"; "tactics.ml"; "drule.ml"; "bool.ml";
1023    "equal.ml"; "printer.ml"; "parser.ml"; "preterm.ml"; "nets.ml";
1024    "basics.ml"; "fusion.ml"; "lib.ml"; "sys.ml"];;
1025
1026   let the_overload_skeletons = [("real_interval", `:A`); ("segment", `:A`); ("interval", `:A`);
1027    ("**", `:A->B->C`); ("norm", `:A->real`); ("gcd", `:A#A->A`);
1028    ("coprime", `:A#A->bool`); ("mod", `:A->A->A->bool`);
1029    ("divides", `:A->A->bool`); ("&", `:num->A`); ("min", `:A->A->A`);
1030    ("max", `:A->A->A`); ("abs", `:A->A`); ("inv", `:A->A`);
1031    ("pow", `:A->num->A`); ("--", `:A->A`); (">=", `:A->A->bool`);
1032    (">", `:A->A->bool`); ("<=", `:A->A->bool`); ("<", `:A->A->bool`);
1033    ("/", `:A->A->A`); ("*", `:A->A->A`); ("-", `:A->A->A`);
1034    ("+", `:A->A->A`)];;
1035
1036   let the_interface =   [("vol", ("measure", `:(real^3->bool)->real`));
1037    ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
1038    ("+", ("vector_add", `:real^N->real^N->real^N`));
1039    ("-", ("vector_sub", `:real^N->real^N->real^N`));
1040    ("--", ("vector_neg", `:real^N->real^N`));
1041    ("norm", ("vector_norm", `:real^N->real`));
1042    ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
1043    ("real_interval",
1044     ("closed_real_interval", `:(real#real)list->real->bool`));
1045    ("real_interval", ("open_real_interval", `:real#real->real->bool`));
1046    ("+", ("real_add", `:real->real->real`));
1047    ("-", ("real_sub", `:real->real->real`));
1048    ("*", ("real_mul", `:real->real->real`));
1049    ("/", ("real_div", `:real->real->real`));
1050    ("<", ("real_lt", `:real->real->bool`));
1051    ("<=", ("real_le", `:real->real->bool`));
1052    (">", ("real_gt", `:real->real->bool`));
1053    (">=", ("real_ge", `:real->real->bool`));
1054    ("--", ("real_neg", `:real->real`));
1055    ("pow", ("real_pow", `:real->num->real`));
1056    ("inv", ("real_inv", `:real->real`));
1057    ("abs", ("real_abs", `:real->real`));
1058    ("max", ("real_max", `:real->real->real`));
1059    ("min", ("real_min", `:real->real->real`));
1060    ("&", ("real_of_num", `:num->real`));
1061    ("mod", ("real_mod", `:real->real->real->bool`));
1062    ("inv", ("complex_inv", `:real^2->real^2`));
1063    ("pow", ("complex_pow", `:real^2->num->real^2`));
1064    ("/", ("complex_div", `:real^2->real^2->real^2`));
1065    ("*", ("complex_mul", `:real^2->real^2->real^2`));
1066    ("-", ("vector_sub", `:real^2->real^2->real^2`));
1067    ("+", ("vector_add", `:real^2->real^2->real^2`));
1068    ("--", ("vector_neg", `:real^2->real^2`));
1069    ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
1070    ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
1071    ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
1072    ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
1073    ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
1074    ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
1075    ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
1076    ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
1077    ("--", ("matrix_neg", `:real^N^M->real^N^M`));
1078    ("dist", ("distance", `:real^N#real^N->real`));
1079    ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
1080    ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
1081    ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
1082    (">=", (">=", `:num->num->bool`));
1083    ("divides", ("num_divides", `:num->num->bool`));
1084    ("mod", ("num_mod", `:num->num->num->bool`));
1085    ("coprime", ("num_coprime", `:num#num->bool`));
1086    ("gcd", ("num_gcd", `:num#num->num`));
1087    ("gcd", ("int_gcd", `:int#int->int`));
1088    ("coprime", ("int_coprime", `:int#int->bool`));
1089    ("mod", ("int_mod", `:int->int->int->bool`));
1090    ("divides", ("int_divides", `:int->int->bool`));
1091    ("&", ("int_of_num", `:num->int`));
1092    ("min", ("int_min", `:int->int->int`));
1093    ("max", ("int_max", `:int->int->int`)); ("abs", ("int_abs", `:int->int`));
1094    ("pow", ("int_pow", `:int->num->int`)); ("--", ("int_neg", `:int->int`));
1095    (">=", ("int_ge", `:int->int->bool`));
1096    (">", ("int_gt", `:int->int->bool`));
1097    ("<=", ("int_le", `:int->int->bool`));
1098    ("<", ("int_lt", `:int->int->bool`));
1099    ("*", ("int_mul", `:int->int->int`));
1100    ("-", ("int_sub", `:int->int->int`));
1101    ("+", ("int_add", `:int->int->int`));
1102    ("&", ("hreal_of_num", `:num->hreal`));
1103    ("<=>", ("=", `:bool->bool->bool`))];;
1104
1105   let the_types = [("net", 1); ("topology", 1); ("3", 0); ("2", 0); ("finite_sum", 2);
1106    ("cart", 2); ("finite_image", 1); ("int", 0); ("real", 0); ("hreal", 0);
1107    ("nadd", 0); ("char", 0); ("list", 1); ("option", 1); ("sum", 2);
1108    ("recspace", 1); ("num", 0); ("ind", 0); ("prod", 2); ("1", 0);
1109    ("bool", 0); ("fun", 2)];;
1110
1111 end;;
1112
1113 module Snapshot_flyspeck_init_2010_02_11 : Snapshot_type = struct
1114
1115   let the_constants = Snapshot_v220_7_31_2009.the_constants;;
1116   let the_loaded_files = Snapshot_v220_7_31_2009.the_loaded_files;;
1117   let the_types = Snapshot_v220_7_31_2009.the_types;;
1118   let the_overload_skeletons = Snapshot_v220_7_31_2009.the_overload_skeletons;;
1119
1120 (*
1121
1122 (* start with the hol-light snapshot v220_7_31_2009 then  *)
1123 prioritize_complex();; (* lowest priority *)
1124 prioritize_int();;
1125 prioritize_num();;
1126 prioritize_vector();;
1127 prioritize_real();;  (* highest priority *)
1128
1129 *)
1130
1131   let the_interface =
1132   [("+", ("real_add", `:real->real->real`));
1133    ("-", ("real_sub", `:real->real->real`));
1134    ("*", ("real_mul", `:real->real->real`));
1135    ("/", ("real_div", `:real->real->real`));
1136    ("<", ("real_lt", `:real->real->bool`));
1137    ("<=", ("real_le", `:real->real->bool`));
1138    (">", ("real_gt", `:real->real->bool`));
1139    (">=", ("real_ge", `:real->real->bool`));
1140    ("--", ("real_neg", `:real->real`));
1141    ("pow", ("real_pow", `:real->num->real`));
1142    ("inv", ("real_inv", `:real->real`));
1143    ("abs", ("real_abs", `:real->real`));
1144    ("max", ("real_max", `:real->real->real`));
1145    ("min", ("real_min", `:real->real->real`));
1146    ("&", ("real_of_num", `:num->real`));
1147    ("mod", ("real_mod", `:real->real->real->bool`));
1148    ("+", ("vector_add", `:real^N->real^N->real^N`));
1149    ("-", ("vector_sub", `:real^N->real^N->real^N`));
1150    ("--", ("vector_neg", `:real^N->real^N`));
1151    ("norm", ("vector_norm", `:real^N->real`));
1152    ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
1153    ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
1154    ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
1155    ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
1156    (">=", (">=", `:num->num->bool`));
1157    ("divides", ("num_divides", `:num->num->bool`));
1158    ("mod", ("num_mod", `:num->num->num->bool`));
1159    ("coprime", ("num_coprime", `:num#num->bool`));
1160    ("gcd", ("num_gcd", `:num#num->num`));
1161    ("+", ("int_add", `:int->int->int`));
1162    ("-", ("int_sub", `:int->int->int`));
1163    ("*", ("int_mul", `:int->int->int`));
1164    ("<", ("int_lt", `:int->int->bool`));
1165    ("<=", ("int_le", `:int->int->bool`));
1166    (">", ("int_gt", `:int->int->bool`));
1167    (">=", ("int_ge", `:int->int->bool`)); ("--", ("int_neg", `:int->int`));
1168    ("pow", ("int_pow", `:int->num->int`)); ("abs", ("int_abs", `:int->int`));
1169    ("max", ("int_max", `:int->int->int`));
1170    ("min", ("int_min", `:int->int->int`));
1171    ("&", ("int_of_num", `:num->int`));
1172    ("divides", ("int_divides", `:int->int->bool`));
1173    ("mod", ("int_mod", `:int->int->int->bool`));
1174    ("coprime", ("int_coprime", `:int#int->bool`));
1175    ("gcd", ("int_gcd", `:int#int->int`));
1176    ("inv", ("complex_inv", `:real^2->real^2`));
1177    ("pow", ("complex_pow", `:real^2->num->real^2`));
1178    ("/", ("complex_div", `:real^2->real^2->real^2`));
1179    ("*", ("complex_mul", `:real^2->real^2->real^2`));
1180    ("-", ("vector_sub", `:real^2->real^2->real^2`));
1181    ("+", ("vector_add", `:real^2->real^2->real^2`));
1182    ("--", ("vector_neg", `:real^2->real^2`));
1183    ("vol", ("measure", `:(real^3->bool)->real`));
1184    ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
1185    ("real_interval",
1186     ("closed_real_interval", `:(real#real)list->real->bool`));
1187    ("real_interval", ("open_real_interval", `:real#real->real->bool`));
1188    ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
1189    ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
1190    ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
1191    ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
1192    ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
1193    ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
1194    ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
1195    ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
1196    ("--", ("matrix_neg", `:real^N^M->real^N^M`));
1197    ("dist", ("distance", `:real^N#real^N->real`));
1198    ("&", ("hreal_of_num", `:num->hreal`));
1199    ("<=>", ("=", `:bool->bool->bool`))];;
1200
1201  end;;
1202