(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: General                                                 *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-10                                                           *)
(* ========================================================================== *)

(* 
store data from different HOL Light snapshots to make it easier to make
an upgrade from one snapshot to the next. 
*)



module type Snapshot_type = sig
  val the_constants :  (string * hol_type) list 
  val the_loaded_files : string list
  val the_overload_skeletons : (string*hol_type) list
  val the_interface : (string * (string * hol_type)) list
  val the_types:(string*int) list
end;;

module Snapshot_utility = struct

(* This was used to make printable manufactured types.  No more `:?467346` *)

let clean_ty ty = 
   let fr = (union (tyvars ty) []) in
   let alpha = map (mk_vartype o (String.make 1) o (char_of_int)) (65--(65+List.length(fr))) in
   let  alphafr = subtract alpha fr in
   let sel = filter (fun t ->  (dest_vartype t).[0]='?')  fr in
   type_subst (map (fun t-> (List.nth alphafr t,List.nth sel t)) (0--(List.length sel - 1))) ty;;

(*
0;;
#print_length 10000;;
map (fun (t,u) -> (t, clean_ty u)) (constants());;
map fst !loaded_files;;
!the_overload_skeletons;;
map (fun (t,(u,v)) -> (t,(u,clean_ty v))) (!the_interface);;
types();;
#print_length 500;;
*)

end;;


module Snapshot_v220_7_29_2009 : Snapshot_type = struct

  let the_types =  [("net", 1); ("topology", 1); ("3", 0); ("2", 0); ("finite_sum", 2);
   ("cart", 2); ("finite_image", 1); ("int", 0); ("real", 0); ("hreal", 0);
   ("nadd", 0); ("char", 0); ("list", 1); ("option", 1); ("sum", 2);
   ("recspace", 1); ("num", 0); ("ind", 0); ("prod", 2); ("1", 0);
   ("bool", 0); ("fun", 2)];;

  let the_loaded_files =  ["flyspeck.ml"; "wlog_examples.ml"; "wlog.ml"; "real.ml"; "measure.ml";
   "card.ml"; "wo.ml"; "geom.ml"; "transc.ml"; "canal.ml"; "complex.ml";
   "integration.ml"; "analysis.ml"; "dimension.ml"; "convex.ml";
   "topology.ml"; "iter.ml"; "floor.ml"; "cross.ml"; "determinants.ml";
   "products.ml"; "permutations.ml"; "vectors.ml"; "misc.ml"; "database.ml";
   "help.ml"; "define.ml"; "cart.ml"; "iter.ml"; "sets.ml"; "int.ml";
   "calc_rat.ml"; "real.ml"; "realarith.ml"; "calc_int.ml"; "realax.ml";
   "list.ml"; "ind-types.ml"; "grobner.ml"; "normalizer.ml"; "calc_num.ml";
   "wf.ml"; "arith.ml"; "num.ml"; "pair.ml"; "recursion.ml"; "quot.ml";
   "meson.ml"; "canon.ml"; "trivia.ml"; "class.ml"; "ind-defs.ml";
   "theorems.ml"; "simp.ml"; "itab.ml"; "tactics.ml"; "drule.ml"; "bool.ml";
   "equal.ml"; "printer.ml"; "parser.ml"; "preterm.ml"; "nets.ml";
   "basics.ml"; "fusion.ml"; "lib.ml"; "sys.ml"];;

  let the_overload_skeletons = 
    [("real_interval", `:A`); ("segment", `:A`); ("interval", `:A`);
   ("**", `:A->B->C`); ("norm", `:A->real`); ("gcd", `:A#A->A`);
   ("coprime", `:A#A->bool`); ("mod", `:A->A->A->bool`);
   ("divides", `:A->A->bool`); ("&", `:num->A`); ("min", `:A->A->A`);
   ("max", `:A->A->A`); ("abs", `:A->A`); ("inv", `:A->A`);
   ("pow", `:A->num->A`); ("--", `:A->A`); (">=", `:A->A->bool`);
   (">", `:A->A->bool`); ("<=", `:A->A->bool`); ("<", `:A->A->bool`);
   ("/", `:A->A->A`); ("*", `:A->A->A`); ("-", `:A->A->A`);
   ("+", `:A->A->A`)];;

(* this should be regenerated. It was not captured at the right moment *)
  let the_interface =  
  [("+", ("real_add", `:real->real->real`));
   ("-", ("real_sub", `:real->real->real`));
   ("*", ("real_mul", `:real->real->real`));
   ("/", ("real_div", `:real->real->real`));
   ("<", ("real_lt", `:real->real->bool`));
   ("<=", ("real_le", `:real->real->bool`));
   (">", ("real_gt", `:real->real->bool`));
   (">=", ("real_ge", `:real->real->bool`));
   ("--", ("real_neg", `:real->real`));
   ("pow", ("real_pow", `:real->num->real`));
   ("inv", ("real_inv", `:real->real`));
   ("abs", ("real_abs", `:real->real`));
   ("max", ("real_max", `:real->real->real`));
   ("min", ("real_min", `:real->real->real`));
   ("&", ("real_of_num", `:num->real`));
   ("mod", ("real_mod", `:real->real->real->bool`));
   ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
   ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
   ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
   (">=", (">=", `:num->num->bool`));
   ("divides", ("num_divides", `:num->num->bool`));
   ("mod", ("num_mod", `:num->num->num->bool`));
   ("coprime", ("num_coprime", `:num#num->bool`));
   ("gcd", ("num_gcd", `:num#num->num`));
   ("vol", ("measure", `:(real^3->bool)->real`));
   ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
   ("+", ("vector_add", `:real^N->real^N->real^N`));
   ("-", ("vector_sub", `:real^N->real^N->real^N`));
   ("--", ("vector_neg", `:real^N->real^N`));
   ("norm", ("vector_norm", `:real^N->real`));
   ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
   ("real_interval",
    ("closed_real_interval", `:(real#real)list->real->bool`));
   ("real_interval", ("open_real_interval", `:real#real->real->bool`));
   ("inv", ("complex_inv", `:real^2->real^2`));
   ("pow", ("complex_pow", `:real^2->num->real^2`));
   ("/", ("complex_div", `:real^2->real^2->real^2`));
   ("*", ("complex_mul", `:real^2->real^2->real^2`));
   ("-", ("vector_sub", `:real^2->real^2->real^2`));
   ("+", ("vector_add", `:real^2->real^2->real^2`));
   ("--", ("vector_neg", `:real^2->real^2`));
   ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
   ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
   ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
   ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
   ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
   ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
   ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
   ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
   ("--", ("matrix_neg", `:real^N^M->real^N^M`));
   ("dist", ("distance", `:real^N#real^N->real`));
   ("gcd", ("int_gcd", `:int#int->int`));
   ("coprime", ("int_coprime", `:int#int->bool`));
   ("mod", ("int_mod", `:int->int->int->bool`));
   ("divides", ("int_divides", `:int->int->bool`));
   ("&", ("int_of_num", `:num->int`));
   ("min", ("int_min", `:int->int->int`));
   ("max", ("int_max", `:int->int->int`)); ("abs", ("int_abs", `:int->int`));
   ("pow", ("int_pow", `:int->num->int`)); ("--", ("int_neg", `:int->int`));
   (">=", ("int_ge", `:int->int->bool`));
   (">", ("int_gt", `:int->int->bool`));
   ("<=", ("int_le", `:int->int->bool`));
   ("<", ("int_lt", `:int->int->bool`));
   ("*", ("int_mul", `:int->int->int`));
   ("-", ("int_sub", `:int->int->int`));
   ("+", ("int_add", `:int->int->int`));
   ("&", ("hreal_of_num", `:num->hreal`));
   ("<=>", ("=", `:bool->bool->bool`))];;

  let the_constants = 
  [("SDIFF", `:(A->bool)->(A->bool)->A->bool`);
   ("vol_ball_wedge", `:real^3->real^3->real^3->real^3->real->real`);
   ("vol_rect", `:real^A->real^B->real`);
   ("vol_conv", `:real^A->real^A->real^A->real^A->real`);
   ("vol_conic_cap_wedge",
    `:real^3->real^3->real^3->real^3->real->real->real`);
   ("vol_frustt_wedge", `:real^3->real^3->real^3->real^3->real->real->real`);
   ("vol_solid_triangle", `:real^A->real^A->real^A->real^A->real->real`);
   ("primitive", `:(real^3->bool)->bool`);
   ("circular_cone", `:(real^3->bool)->bool`);
   ("c_cone", `:real^3#real^3#real->real^3->bool`);
   ("sphere", `:(real^3->bool)->bool`);
   ("rect", `:real^3->real^3->real^3->bool`);
   ("solid_triangle", `:real^A->(real^A->bool)->real->real^A->bool`);
   ("cone0", `:real^A->(real^A->bool)->real^A->bool`);
   ("cone", `:real^A->(real^A->bool)->real^A->bool`);
   ("dihV", `:real^A->real^A->real^A->real^A->real`);
   ("opposite", `:real^N->real^N->(real^N->bool)->bool`);
   ("arcV", `:real^A->real^A->real^A->real`);
   ("wedge", `:real^3->real^3->real^3->real^3->real^3->bool`);
   ("azim", `:real^3->real^3->real^3->real^3->real`);
   ("orthonormal", `:real^3->real^3->real^3->bool`);
   ("conic_cap", `:real^A->real^A->real->real->real^A->bool`);
   ("ellipsoid", `:real^3->real->real^3->bool`);
   ("normball", `:real^A->real->real^A->bool`);
   ("scale", `:real^3->real^3->real^3`);
   ("frustt", `:real^A->real^A->real->real->real^A->bool`);
   ("frustum", `:real^N->real^N->real->real->real->real^N->bool`);
   ("rcone_eq", `:real^A->real^A->real->real^A->bool`);
   ("rcone_ge", `:real^A->real^A->real->real^A->bool`);
   ("rcone_gt", `:real^A->real^A->real->real^A->bool`);
   ("rconesgn", `:(real->real->bool)->real^A->real^A->real->real^A->bool`);
   ("delta_x", `:real->real->real->real->real->real->real`);
   ("conv0", `:(real^A->bool)->real^A->bool`);
   ("aff_le", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("aff_lt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("aff_ge", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("aff_gt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("sgn_le", `:real->bool`); ("sgn_lt", `:real->bool`);
   ("sgn_ge", `:real->bool`); ("sgn_gt", `:real->bool`);
   ("affsign", `:(real->bool)->(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("lin_combo", `:(real^N->bool)->(real^N->real)->real^N`);
   ("pad2d3d", `:real^2->real^3`); ("plane", `:(real^A->bool)->bool`);
   ("slice", `:num->real->(real^A->bool)->real^B->bool`);
   ("pushin", `:num->B->B^A->B^C`); ("dropout", `:num->real^N->real^M`);
   ("real_measure", `:(real->bool)->real`);
   ("real_measurable", `:(real->bool)->bool`);
   ("has_real_measure", `:(real->bool)->real->bool`);
   ("absolutely_real_integrable_on", `:(real->real)->(real->bool)->bool`);
   ("real_negligible", `:(real->bool)->bool`);
   ("real_integral", `:(real->bool)->(real->real)->real`);
   ("real_integrable_on", `:(real->real)->(real->bool)->bool`);
   ("has_real_integral", `:(real->real)->real->(real->bool)->bool`);
   ("closed_real_interval", `:(real#real)list->real->bool`);
   ("open_real_interval", `:real#real->real->bool`);
   ("is_realinterval", `:(real->bool)->bool`);
   ("real_differentiable_on", `:(real->real)->(real->bool)->bool`);
   ("higher_real_derivative", `:num->(real->real)->real->real`);
   ("real_derivative", `:(real->real)->real->real`);
   ("real_differentiable", `:(real->real)->(real)net->bool`);
   ("has_real_derivative", `:(real->real)->real->(real)net->bool`);
   ("real_continuous_on", `:(real->real)->(real->bool)->bool`);
   ("real_continuous", `:(A->real)->(A)net->bool`);
   ("at_neginfinity", `:(real)net`); ("at_posinfinity", `:(real)net`);
   ("atreal", `:real->(real)net`);
   ("real_summable", `:(num->bool)->(num->real)->bool`);
   ("real_infsum", `:(num->bool)->(num->real)->real`);
   ("real_sums", `:(num->real)->real->(num->bool)->bool`);
   ("--->", `:(A->real)->real->(A)net->bool`);
   ("real_compact", `:(real->bool)->bool`);
   ("real_bounded", `:(real->bool)->bool`);
   ("euclideanreal", `:(real)topology`);
   ("real_closed", `:(real->bool)->bool`);
   ("real_open", `:(real->bool)->bool`);
   ("measure", `:(real^A->bool)->real`);
   ("measurable", `:(real^A->bool)->bool`);
   ("has_measure", `:(real^A->bool)->real->bool`);
   ("*_c", `:(A->bool)->(B->bool)->A#B->bool`);
   ("+_c", `:(A->bool)->(B->bool)->A+B->bool`);
   ("ordinal", `:(A#A->bool)->bool`);
   ("linseg", `:(A#A->bool)->A->A#A->bool`);
   ("inseg", `:(A#A->bool)->(A#A->bool)->bool`);
   ("woset", `:(A#A->bool)->bool`);
   ("chain", `:(A#A->bool)->(A->bool)->bool`);
   ("poset", `:(A#A->bool)->bool`); ("fl", `:(A#A->bool)->A->bool`);
   ("less", `:(A#A->bool)->A#A->bool`);
   ("angle", `:real^A#real^A#real^A->real`);
   ("vector_angle", `:real^A->real^A->real`); ("acs", `:real->real`);
   ("asn", `:real->real`); ("cacs", `:real^2->real^2`);
   ("casn", `:real^2->real^2`); ("atn", `:real->real`);
   ("catn", `:real^2->real^2`); ("unwinding", `:real^2->real^2`);
   ("cpow", `:real^2->real^2->real^2`); ("clog", `:real^2->real^2`);
   ("tan", `:real->real`); ("ctan", `:real^2->real^2`);
   ("rotate2d", `:real->real^2->real^2`); ("Arg", `:real^2->real`);
   ("pi", `:real`); ("log", `:real->real`); ("cos", `:real->real`);
   ("sin", `:real->real`); ("exp", `:real->real`);
   ("csin", `:real^2->real^2`); ("ccos", `:real^2->real^2`);
   ("cexp", `:real^2->real^2`);
   ("analytic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
   ("holomorphic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
   ("higher_complex_derivative", `:num->(real^2->real^2)->real^2->real^2`);
   ("complex_derivative", `:(real^2->real^2)->real^2->real^2`);
   ("complex_differentiable", `:(real^2->real^2)->(real^2)net->bool`);
   ("has_complex_derivative", `:(real^2->real^2)->real^2->(real^2)net->bool`);
   ("cproduct", `:(A->bool)->(A->real^2)->real^2`);
   ("real", `:real^2->bool`); ("csqrt", `:real^2->real^2`);
   ("cnj", `:real^2->real^2`); ("complex_pow", `:real^2->num->real^2`);
   ("complex_div", `:real^2->real^2->real^2`);
   ("complex_inv", `:real^2->real^2`);
   ("complex_mul", `:real^2->real^2->real^2`); ("ii", `:real^2`);
   ("Cx", `:real->real^2`); ("complex", `:real#real->real^2`);
   ("Im", `:real^2->real`); ("Re", `:real^2->real`);
   ("absolutely_integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("negligible", `:(real^A->bool)->bool`);
   ("indicator", `:(real^M->bool)->real^M->real^1`);
   ("division_points",
    `:(real^N->bool)->((real^N->bool)->bool)->num#real->bool`);
   ("lifted", `:(A->A->B)->(A)option->(A)option->(B)option`);
   ("operative", `:(A->A->A)->((real^N->bool)->A)->bool`);
   ("integral", `:(real^A->bool)->(real^A->real^B)->real^B`);
   ("integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("has_integral", `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
   ("has_integral_compact_interval",
    `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
   ("fine", `:(A->B->bool)->(A#(B->bool)->bool)->bool`);
   ("tagged_division_of",
    `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
   ("tagged_partial_division_of",
    `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
   ("division_of", `:((real^A->bool)->bool)->(real^A->bool)->bool`);
   ("gauge", `:(real^A->real^A->bool)->bool`);
   ("content", `:(real^M->bool)->real`);
   ("interval_lowerbound", `:(real^M->bool)->real^M`);
   ("interval_upperbound", `:(real^M->bool)->real^M`);
   ("vector_derivative", `:(real^1->real^N)->(real^1)net->real^N`);
   ("has_vector_derivative", `:(real^1->real^A)->real^A->(real^1)net->bool`);
   ("jacobian", `:(real^A->real^B)->(real^A)net->real^A^B`);
   ("frechet_derivative", `:(real^A->real^B)->(real^A)net->real^A->real^B`);
   ("differentiable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("differentiable", `:(real^B->real^A)->(real^B)net->bool`);
   ("has_derivative",
    `:(real^B->real^A)->(real^B->real^A)->(real^B)net->bool`);
   ("interval_bij", `:real^N#real^N->real^N#real^N->real^N->real^N`);
   ("retract_of", `:(real^A->bool)->(real^A->bool)->bool`);
   ("retraction", `:(real^N->bool)#(real^N->bool)->(real^N->real^N)->bool`);
   ("reduced", `:((num->num)->num->num)->num->(num->num)->num`);
   ("ksimplex", `:num->num->((num->num)->bool)->bool`);
   ("kle", `:num->(num->num)->(num->num)->bool`);
   ("path_connected", `:(real^A->bool)->bool`);
   ("path_component", `:(real^A->bool)->real^A->real^A->bool`);
   ("linepath", `:real^A#real^A->real^1->real^A`);
   ("shiftpath", `:real^1->(real^1->real^N)->real^1->real^N`);
   ("arc", `:(real^1->real^N)->bool`);
   ("simple_path", `:(real^1->real^N)->bool`);
   ("++", `:(real^1->A)->(real^1->A)->real^1->A`);
   ("reversepath", `:(real^1->real^N)->real^1->real^N`);
   ("path_image", `:(real^1->real^N)->real^N->bool`);
   ("pathfinish", `:(real^1->real^N)->real^N`);
   ("pathstart", `:(real^1->real^N)->real^N`);
   ("path", `:(real^1->real^N)->bool`);
   ("extreme_point_of", `:real^A->(real^A->bool)->bool`);
   ("face_of", `:(real^A->bool)->(real^A->bool)->bool`);
   ("relative_interior", `:(real^A->bool)->real^A->bool`);
   ("starlike", `:(real^A->bool)->bool`);
   ("epigraph",
    `:(real^N->bool)->(real^N->real)->real^(N,1)finite_sum->bool`);
   ("convex_on", `:(real^A->real)->(real^A->bool)->bool`);
   ("coplanar", `:(real^A->bool)->bool`);
   ("affine_dependent", `:(real^N->bool)->bool`);
   ("conic", `:(real^A->bool)->bool`); ("convex", `:(real^A->bool)->bool`);
   ("affine", `:(real^A->bool)->bool`);
   ("closest_point", `:(real^A->bool)->real^A->real^A`);
   ("from", `:num->num->bool`);
   ("summable", `:(num->bool)->(num->real^A)->bool`);
   ("infsum", `:(num->bool)->(num->real^A)->real^A`);
   ("sums", `:(num->real^A)->real^A->(num->bool)->bool`);
   ("homeomorphic", `:(real^A->bool)->(real^B->bool)->bool`);
   ("homeomorphism",
    `:(real^B->bool)#(real^A->bool)->(real^B->real^A)#(real^A->real^B)->bool`);
   ("open_segment", `:real^A#real^A->real^A->bool`);
   ("closed_segment", `:(real^A#real^A)list->real^A->bool`);
   ("is_interval", `:(real^N->bool)->bool`);
   ("closed_interval", `:(real^N#real^N)list->real^N->bool`);
   ("open_interval", `:real^N#real^N->real^N->bool`);
   ("diameter", `:(real^A->bool)->real`);
   ("connected_component", `:(real^A->bool)->real^A->real^A->bool`);
   ("uniformly_continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("continuous", `:(B->real^A)->(B)net->bool`);
   ("complete", `:(real^N->bool)->bool`); ("cauchy", `:(num->real^N)->bool`);
   ("compact", `:(real^N->bool)->bool`);
   ("bounded", `:(real^N->bool)->bool`); ("netlimit", `:(A)net->A`);
   ("lim", `:(A)net->(A->real^B)->real^B`);
   ("-->", `:(B->real^A)->real^A->(B)net->bool`);
   ("eventually", `:(A->bool)->(A)net->bool`);
   ("trivial_limit", `:(A)net->bool`);
   ("in_direction", `:real^A->real^A->(real^A)net`);
   ("within", `:(A)net->(A->bool)->(A)net`); ("sequentially", `:(num)net`);
   ("at_infinity", `:(real^A)net`); ("at", `:real^A->(real^A)net`);
   ("netord", `:(A)net->A->A->bool`); ("mk_net", `:(A->A->bool)->(A)net`);
   ("frontier", `:(real^A->bool)->real^A->bool`);
   ("closure", `:(real^A->bool)->real^A->bool`);
   ("interior", `:(real^A->bool)->real^A->bool`);
   ("limit_point_of", `:real^A->(real^A->bool)->bool`);
   ("connected", `:(real^A->bool)->bool`);
   ("cball", `:real^A#real->real^A->bool`);
   ("ball", `:real^A#real->real^A->bool`);
   ("euclidean", `:(real^A)topology`); ("closed", `:(real^N->bool)->bool`);
   ("open", `:(real^A->bool)->bool`);
   ("subtopology", `:(A)topology->(A->bool)->(A)topology`);
   ("closed_in", `:(A)topology->(A->bool)->bool`);
   ("topspace", `:(A)topology->A->bool`);
   ("open_in", `:(A)topology->(A->bool)->bool`);
   ("topology", `:((A->bool)->bool)->(A)topology`);
   ("istopology", `:((A->bool)->bool)->bool`);
   ("ITER", `:num->(A->A)->A->A`); ("frac", `:real->real`);
   ("floor", `:real->real`); ("integer", `:real->bool`);
   ("cross", `:real^3->real^3->real^3`);
   ("rotoinversion_matrix", `:real^A^A->bool`);
   ("rotation_matrix", `:real^A^A->bool`);
   ("orthogonal_matrix", `:real^N^N->bool`);
   ("orthogonal_transformation", `:(real^N->real^N)->bool`);
   ("det", `:real^N^N->real`); ("trace", `:real^N^N->real`);
   ("product", `:(A->bool)->(A->real)->real`); ("sign", `:(A->A)->real`);
   ("evenperm", `:(A->A)->bool`); ("permutation", `:(A->A)->bool`);
   ("swapseq", `:num->(A->A)->bool`); ("swap", `:A#A->A->A`);
   ("inverse", `:(B->A)->A->B`); ("permutes", `:(A->A)->(A->bool)->bool`);
   ("midpoint", `:real^A#real^A->real^A`);
   ("between", `:real^A->real^A#real^A->bool`);
   ("collinear", `:(real^A->bool)->bool`); ("infnorm", `:real^N->real`);
   ("rank", `:real^M^N->num`); ("columnvector", `:real^N->real^1^N`);
   ("rowvector", `:real^N->real^N^1`); ("dim", `:(real^A->bool)->num`);
   ("independent", `:(real^A->bool)->bool`);
   ("dependent", `:(real^A->bool)->bool`);
   ("span", `:(real^A->bool)->real^A->bool`);
   ("subspace", `:(real^A->bool)->bool`); ("drop", `:real^1->real`);
   ("lift", `:real->real^1`); ("onorm", `:(real^M->real^N)->real`);
   ("matrix", `:(real^M->real^N)->real^M^N`);
   ("matrix_inv", `:real^N^M->real^M^N`); ("invertible", `:real^N^M->bool`);
   ("columns", `:real^N^M->real^M->bool`);
   ("rows", `:real^N^M->real^N->bool`); ("column", `:num->real^N^M->real^M`);
   ("row", `:num->real^N^M->real^N`); ("transp", `:real^N^M->real^M^N`);
   ("mat", `:num->real^N^M`);
   ("vector_matrix_mul", `:real^M->real^N^M->real^N`);
   ("matrix_vector_mul", `:real^N^M->real^N->real^M`);
   ("matrix_mul", `:real^N^M->real^P^N->real^P^M`);
   ("matrix_sub", `:real^N^M->real^N^M->real^N^M`);
   ("matrix_add", `:real^N^M->real^N^M->real^N^M`);
   ("matrix_neg", `:real^N^M->real^N^M`);
   ("adjoint", `:(real^M->real^N)->real^N->real^M`);
   ("bilinear", `:(real^A->real^B->real^C)->bool`);
   ("linear", `:(real^M->real^N)->bool`);
   ("orthogonal", `:real^A->real^A->bool`); ("basis", `:num->real^A`);
   ("vsum", `:(A->bool)->(A->real^N)->real^N`);
   ("distance", `:real^A#real^A->real`); ("vector_norm", `:real^A->real`);
   ("dot", `:real^N->real^N->real`); ("vec", `:num->real^N`);
   ("%", `:real->real^N->real^N`); ("vector_neg", `:real^N->real^N`);
   ("vector_sub", `:real^N->real^N->real^N`);
   ("vector_add", `:real^N->real^N->real^N`); ("sqrt", `:real->real`);
   ("hull", `:((A->bool)->bool)->(A->bool)->A->bool`);
   ("inf", `:(real->bool)->real`); ("sup", `:(real->bool)->real`);
   ("superadmissible",
    `:(A->A->bool)->((A->C)->B->bool)->(B->A)->((A->C)->B->C)->bool`);
   ("tailadmissible",
    `:(A->A->bool)->((A->B)->P->bool)->(P->A)->((A->B)->P->B)->bool`);
   ("admissible",
    `:(B->A->bool)->((B->C)->D->bool)->(D->A)->((B->C)->D->E)->bool`);
   ("CASEWISE", `:((A->C)#(B->A->D))list->B->C->D`);
   ("vector", `:(A)list->A^N`);
   ("dest_auto_define_finite_type_3", `:3->num`);
   ("mk_auto_define_finite_type_3", `:num->3`);
   ("dest_auto_define_finite_type_2", `:2->num`);
   ("mk_auto_define_finite_type_2", `:num->2`);
   ("sndcart", `:A^(M,N)finite_sum->A^N`);
   ("fstcart", `:A^(M,N)finite_sum->A^M`);
   ("pastecart", `:A^M->A^N->A^(M,N)finite_sum`);
   ("dest_finite_sum", `:(A,B)finite_sum->num`);
   ("mk_finite_sum", `:num->(A,B)finite_sum`); ("lambda", `:(num->A)->A^B`);
   ("$", `:B^A->num->B`); ("dest_cart", `:A^B->(B)finite_image->A`);
   ("mk_cart", `:((B)finite_image->A)->A^B`);
   ("dest_finite_image", `:(A)finite_image->num`);
   ("finite_index", `:num->(A)finite_image`);
   ("dimindex", `:(A->bool)->num`); ("sum", `:(A->bool)->(A->real)->real`);
   ("nsum", `:(A->bool)->(A->num)->num`);
   ("iterate", `:(B->B->B)->(A->bool)->(A->B)->B`);
   ("support", `:(B->B->B)->(A->B)->(A->bool)->A->bool`);
   ("monoidal", `:(A->A->A)->bool`); ("neutral", `:(A->A->A)->A`);
   ("..", `:num->num->num->bool`); ("COUNTABLE", `:(A->bool)->bool`);
   (">_c", `:(A->bool)->(B->bool)->bool`);
   (">=_c", `:(A->bool)->(B->bool)->bool`);
   ("=_c", `:(A->bool)->(B->bool)->bool`);
   ("<_c", `:(A->bool)->(B->bool)->bool`);
   ("<=_c", `:(A->bool)->(B->bool)->bool`);
   ("PAIRWISE", `:(A->A->bool)->(A)list->bool`);
   ("pairwise", `:(A->A->bool)->(A->bool)->bool`);
   ("list_of_set", `:(A->bool)->(A)list`);
   ("set_of_list", `:(A)list->A->bool`);
   ("CROSS", `:(A->bool)->(B->bool)->A#B->bool`);
   ("HAS_SIZE", `:(A->bool)->num->bool`); ("CARD", `:(A->bool)->num`);
   ("ITSET", `:(A->B->B)->(A->bool)->B->B`);
   ("FINREC", `:(A->B->B)->B->(A->bool)->B->num->bool`);
   ("REST", `:(A->bool)->A->bool`); ("CHOICE", `:(A->bool)->A`);
   ("BIJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
   ("SURJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
   ("INJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
   ("IMAGE", `:(A->B)->(A->bool)->B->bool`);
   ("INFINITE", `:(A->bool)->bool`); ("FINITE", `:(A->bool)->bool`);
   ("SING", `:(A->bool)->bool`); ("DISJOINT", `:(A->bool)->(A->bool)->bool`);
   ("PSUBSET", `:(A->bool)->(A->bool)->bool`);
   ("SUBSET", `:(A->bool)->(A->bool)->bool`);
   ("DELETE", `:(A->bool)->A->A->bool`);
   ("DIFF", `:(A->bool)->(A->bool)->A->bool`);
   ("INTERS", `:((A->bool)->bool)->A->bool`);
   ("INTER", `:(A->bool)->(A->bool)->A->bool`);
   ("UNIONS", `:((A->bool)->bool)->A->bool`);
   ("UNION", `:(A->bool)->(A->bool)->A->bool`); ("UNIV", `:A->bool`);
   ("INSERT", `:A->(A->bool)->A->bool`); ("EMPTY", `:A->bool`);
   ("SETSPEC", `:A->bool->A->bool`); ("GSPEC", `:(A->bool)->A->bool`);
   ("IN", `:A->(A->bool)->bool`); ("num_gcd", `:num#num->num`);
   ("num_coprime", `:num#num->bool`); ("num_mod", `:num->num->num->bool`);
   ("num_divides", `:num->num->bool`); ("num_of_int", `:int->num`);
   ("int_gcd", `:int#int->int`); ("int_coprime", `:int#int->bool`);
   ("int_mod", `:int->int->int->bool`); ("int_divides", `:int->int->bool`);
   ("real_mod", `:real->real->real->bool`);
   ("==", `:A->A->(A->A->bool)->bool`); ("rem", `:int->int->int`);
   ("div", `:int->int->int`); ("int_pow", `:int->num->int`);
   ("int_min", `:int->int->int`); ("int_max", `:int->int->int`);
   ("int_abs", `:int->int`); ("int_mul", `:int->int->int`);
   ("int_sub", `:int->int->int`); ("int_add", `:int->int->int`);
   ("int_neg", `:int->int`); ("int_of_num", `:num->int`);
   ("int_gt", `:int->int->bool`); ("int_ge", `:int->int->bool`);
   ("int_lt", `:int->int->bool`); ("int_le", `:int->int->bool`);
   ("real_of_int", `:int->real`); ("int_of_real", `:real->int`);
   ("is_int", `:real->bool`); ("DECIMAL", `:num->num->real`);
   ("real_min", `:real->real->real`); ("real_max", `:real->real->real`);
   ("real_div", `:real->real->real`); ("real_pow", `:real->num->real`);
   ("real_abs", `:real->real`); ("real_gt", `:real->real->bool`);
   ("real_ge", `:real->real->bool`); ("real_lt", `:real->real->bool`);
   ("real_sub", `:real->real->real`); ("real_inv", `:real->real`);
   ("real_le", `:real->real->bool`); ("real_mul", `:real->real->real`);
   ("real_add", `:real->real->real`); ("real_neg", `:real->real`);
   ("real_of_num", `:num->real`); ("dest_real", `:real->hreal#hreal->bool`);
   ("mk_real", `:(hreal#hreal->bool)->real`);
   ("treal_eq", `:hreal#hreal->hreal#hreal->bool`);
   ("treal_inv", `:hreal#hreal->hreal#hreal`);
   ("treal_le", `:hreal#hreal->hreal#hreal->bool`);
   ("treal_mul", `:hreal#hreal->hreal#hreal->hreal#hreal`);
   ("treal_add", `:hreal#hreal->hreal#hreal->hreal#hreal`);
   ("treal_neg", `:hreal#hreal->hreal#hreal`);
   ("treal_of_num", `:num->hreal#hreal`); ("hreal_inv", `:hreal->hreal`);
   ("hreal_le", `:hreal->hreal->bool`);
   ("hreal_mul", `:hreal->hreal->hreal`);
   ("hreal_add", `:hreal->hreal->hreal`); ("hreal_of_num", `:num->hreal`);
   ("dest_hreal", `:hreal->nadd->bool`);
   ("mk_hreal", `:(nadd->bool)->hreal`); ("nadd_inv", `:nadd->nadd`);
   ("nadd_rinv", `:nadd->num->num`); ("nadd_mul", `:nadd->nadd->nadd`);
   ("nadd_add", `:nadd->nadd->nadd`); ("nadd_le", `:nadd->nadd->bool`);
   ("nadd_of_num", `:num->nadd`); ("nadd_eq", `:nadd->nadd->bool`);
   ("dest_nadd", `:nadd->num->num`); ("mk_nadd", `:(num->num)->nadd`);
   ("is_nadd", `:(num->num)->bool`); ("dist", `:num#num->num`);
   ("ASCII", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
   ("_16756", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
   ("_dest_char", `:char->(bool#bool#bool#bool#bool#bool#bool#bool)recspace`);
   ("_mk_char", `:(bool#bool#bool#bool#bool#bool#bool#bool)recspace->char`);
   ("ZIP", `:(A)list->(B)list->(A#B)list`);
   ("ITLIST2", `:(A->B->C->C)->(A)list->(B)list->C->C`);
   ("ASSOC", `:A->(A#B)list->B`); ("FILTER", `:(A->bool)->(A)list->(A)list`);
   ("EL", `:num->(A)list->A`);
   ("MAP2", `:(A->B->C)->(A)list->(B)list->(C)list`);
   ("ALL2", `:(A->B->bool)->(A)list->(B)list->bool`);
   ("MEM", `:A->(A)list->bool`); ("ITLIST", `:(A->B->B)->(A)list->B->B`);
   ("EX", `:(A->bool)->(A)list->bool`); ("ALL", `:(A->bool)->(A)list->bool`);
   ("NULL", `:(A)list->bool`); ("REPLICATE", `:num->A->(A)list`);
   ("LAST", `:(A)list->A`); ("MAP", `:(A->B)->(A)list->(B)list`);
   ("LENGTH", `:(A)list->num`); ("REVERSE", `:(A)list->(A)list`);
   ("APPEND", `:(A)list->(A)list->(A)list`); ("TL", `:(A)list->(A)list`);
   ("HD", `:(A)list->A`); ("ISO", `:(A->B)->(B->A)->bool`);
   ("CONS", `:A->(A)list->(A)list`); ("NIL", `:(A)list`);
   ("_dest_list", `:(A)list->(A)recspace`);
   ("_mk_list", `:(A)recspace->(A)list`); ("SOME", `:A->(A)option`);
   ("NONE", `:(A)option`); ("_dest_option", `:(A)option->(A)recspace`);
   ("_mk_option", `:(A)recspace->(A)option`); ("OUTR", `:A+B->B`);
   ("OUTL", `:A+B->A`); ("INR", `:B->A+B`); ("INL", `:A->A+B`);
   ("_dest_sum", `:A+B->(A#B)recspace`); ("_mk_sum", `:(A#B)recspace->A+B`);
   ("FNIL", `:num->A`); ("FCONS", `:A->(num->A)->num->A`);
   ("CONSTR", `:num->A->(num->(A)recspace)->(A)recspace`);
   ("BOTTOM", `:(A)recspace`); ("_dest_rec", `:(A)recspace->num->A->bool`);
   ("_mk_rec", `:(num->A->bool)->(A)recspace`);
   ("ZRECSPACE", `:(num->A->bool)->bool`); ("ZBOT", `:num->A->bool`);
   ("ZCONSTR", `:num->A->(num->num->A->bool)->num->A->bool`);
   ("INJP", `:(num->A->bool)->(num->A->bool)->num->A->bool`);
   ("INJF", `:(num->num->A->bool)->num->A->bool`);
   ("INJA", `:A->num->A->bool`); ("INJN", `:num->num->A->bool`);
   ("NUMRIGHT", `:num->num`); ("NUMLEFT", `:num->bool`);
   ("NUMSUM", `:bool->num->num`); ("NUMSND", `:num->num`);
   ("NUMFST", `:num->num`); ("NUMPAIR", `:num->num->num`);
   ("MEASURE", `:(A->num)->A->A->bool`); ("WF", `:(A->A->bool)->bool`);
   ("minimal", `:(num->bool)->num`); ("MIN", `:num->num->num`);
   ("MAX", `:num->num->num`); ("MOD", `:num->num->num`);
   ("DIV", `:num->num->num`); ("FACT", `:num->num`); ("-", `:num->num->num`);
   ("ODD", `:num->bool`); ("EVEN", `:num->bool`); (">", `:num->num->bool`);
   (">=", `:num->num->bool`); ("<", `:num->num->bool`);
   ("<=", `:num->num->bool`); ("EXP", `:num->num->num`);
   ("*", `:num->num->num`); ("BIT1", `:num->num`); ("BIT0", `:num->num`);
   ("+", `:num->num->num`); ("PRE", `:num->num`); ("NUMERAL", `:num->num`);
   ("SUC", `:num->num`); ("_0", `:num`); ("dest_num", `:num->ind`);
   ("mk_num", `:ind->num`); ("NUM_REP", `:ind->bool`); ("IND_0", `:ind`);
   ("IND_SUC", `:ind->ind`); ("ONTO", `:(A->B)->bool`);
   ("ONE_ONE", `:(A->B)->bool`); ("PASSOC", `:((A#B)#C->D)->A#B#C->D`);
   ("UNCURRY", `:(A->B->C)->A#B->C`); ("CURRY", `:(A#B->C)->A->B->C`);
   ("SND", `:A#B->B`); ("FST", `:A#B->A`); (",", `:A->B->A#B`);
   ("REP_prod", `:A#B->A->B->bool`); ("ABS_prod", `:(A->B->bool)->A#B`);
   ("mk_pair", `:A->B->A->B->bool`); ("_FUNCTION", `:(A->B->bool)->A->B`);
   ("_MATCH", `:A->(A->B->bool)->B`);
   ("_GUARDED_PATTERN", `:bool->bool->bool->bool`);
   ("_UNGUARDED_PATTERN", `:bool->bool->bool`);
   ("_SEQPATTERN", `:(A->B->bool)->(A->B->bool)->A->B->bool`);
   ("GEQ", `:A->A->bool`); ("GABS", `:(A->bool)->A`); ("LET_END", `:A->A`);
   ("LET", `:(A->B)->A->B`); ("one", `:1`); ("one_REP", `:1->bool`);
   ("one_ABS", `:bool->1`); ("I", `:A->A`); ("o", `:(B->C)->(A->B)->A->C`);
   ("COND", `:bool->A->A->A`); ("@", `:(A->bool)->A`);
   ("_FALSITY_", `:bool`); ("?!", `:(A->bool)->bool`); ("~", `:bool->bool`);
   ("F", `:bool`); ("\\/", `:bool->bool->bool`); ("?", `:(A->bool)->bool`);
   ("!", `:(A->bool)->bool`); ("==>", `:bool->bool->bool`);
   ("/\\", `:bool->bool->bool`); ("T", `:bool`); ("=", `:A->A->bool`)];;  

end;;


module Snapshot_v220_7_31_2009 : Snapshot_type = struct

  let the_constants =
  [("SDIFF", `:(A->bool)->(A->bool)->A->bool`);
   ("vol_ball_wedge", `:real^3->real^3->real^3->real^3->real->real`);
   ("vol_rect", `:real^A->real^B->real`);
   ("vol_conv", `:real^A->real^A->real^A->real^A->real`);
   ("vol_conic_cap_wedge",
    `:real^3->real^3->real^3->real^3->real->real->real`);
   ("vol_frustt_wedge", `:real^3->real^3->real^3->real^3->real->real->real`);
   ("vol_solid_triangle", `:real^A->real^A->real^A->real^A->real->real`);
   ("primitive", `:(real^3->bool)->bool`);
   ("circular_cone", `:(real^3->bool)->bool`);
   ("c_cone", `:real^3#real^3#real->real^3->bool`);
   ("sphere", `:(real^3->bool)->bool`);
   ("rect", `:real^3->real^3->real^3->bool`);
   ("solid_triangle", `:real^A->(real^A->bool)->real->real^A->bool`);
   ("cone0", `:real^A->(real^A->bool)->real^A->bool`);
   ("cone", `:real^A->(real^A->bool)->real^A->bool`);
   ("dihV", `:real^A->real^A->real^A->real^A->real`);
   ("opposite", `:real^N->real^N->(real^N->bool)->bool`);
   ("wedge", `:real^3->real^3->real^3->real^3->real^3->bool`);
   ("azim", `:real^3->real^3->real^3->real^3->real`);
   ("arcV", `:real^A->real^A->real^A->real`);
   ("orthonormal", `:real^3->real^3->real^3->bool`);
   ("conic_cap", `:real^A->real^A->real->real->real^A->bool`);
   ("ellipsoid", `:real^3->real->real^3->bool`);
   ("normball", `:real^A->real->real^A->bool`);
   ("scale", `:real^3->real^3->real^3`);
   ("frustt", `:real^A->real^A->real->real->real^A->bool`);
   ("frustum", `:real^N->real^N->real->real->real->real^N->bool`);
   ("rcone_eq", `:real^A->real^A->real->real^A->bool`);
   ("rcone_ge", `:real^A->real^A->real->real^A->bool`);
   ("rcone_gt", `:real^A->real^A->real->real^A->bool`);
   ("rconesgn", `:(real->real->bool)->real^A->real^A->real->real^A->bool`);
   ("delta_x", `:real->real->real->real->real->real->real`);
   ("conv0", `:(real^A->bool)->real^A->bool`);
   ("aff_le", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("aff_lt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("aff_ge", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("aff_gt", `:(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("sgn_le", `:real->bool`); ("sgn_lt", `:real->bool`);
   ("sgn_ge", `:real->bool`); ("sgn_gt", `:real->bool`);
   ("affsign", `:(real->bool)->(real^A->bool)->(real^A->bool)->real^A->bool`);
   ("lin_combo", `:(real^N->bool)->(real^N->real)->real^N`);
   ("pad2d3d", `:real^2->real^3`); ("plane", `:(real^A->bool)->bool`);
   ("slice", `:num->real->(real^A->bool)->real^B->bool`);
   ("pushin", `:num->B->B^A->B^C`); ("dropout", `:num->real^N->real^M`);
   ("real_measure", `:(real->bool)->real`);
   ("real_measurable", `:(real->bool)->bool`);
   ("has_real_measure", `:(real->bool)->real->bool`);
   ("absolutely_real_integrable_on", `:(real->real)->(real->bool)->bool`);
   ("real_negligible", `:(real->bool)->bool`);
   ("real_integral", `:(real->bool)->(real->real)->real`);
   ("real_integrable_on", `:(real->real)->(real->bool)->bool`);
   ("has_real_integral", `:(real->real)->real->(real->bool)->bool`);
   ("closed_real_interval", `:(real#real)list->real->bool`);
   ("open_real_interval", `:real#real->real->bool`);
   ("is_realinterval", `:(real->bool)->bool`);
   ("real_differentiable_on", `:(real->real)->(real->bool)->bool`);
   ("higher_real_derivative", `:num->(real->real)->real->real`);
   ("real_derivative", `:(real->real)->real->real`);
   ("real_differentiable", `:(real->real)->(real)net->bool`);
   ("has_real_derivative", `:(real->real)->real->(real)net->bool`);
   ("real_continuous_on", `:(real->real)->(real->bool)->bool`);
   ("real_continuous", `:(A->real)->(A)net->bool`);
   ("at_neginfinity", `:(real)net`); ("at_posinfinity", `:(real)net`);
   ("atreal", `:real->(real)net`);
   ("real_summable", `:(num->bool)->(num->real)->bool`);
   ("real_infsum", `:(num->bool)->(num->real)->real`);
   ("real_sums", `:(num->real)->real->(num->bool)->bool`);
   ("--->", `:(A->real)->real->(A)net->bool`);
   ("real_compact", `:(real->bool)->bool`);
   ("real_bounded", `:(real->bool)->bool`);
   ("euclideanreal", `:(real)topology`);
   ("real_closed", `:(real->bool)->bool`);
   ("real_open", `:(real->bool)->bool`);
   ("measure", `:(real^A->bool)->real`);
   ("measurable", `:(real^A->bool)->bool`);
   ("has_measure", `:(real^A->bool)->real->bool`);
   ("*_c", `:(A->bool)->(B->bool)->A#B->bool`);
   ("+_c", `:(A->bool)->(B->bool)->A+B->bool`);
   ("ordinal", `:(A#A->bool)->bool`);
   ("linseg", `:(A#A->bool)->A->A#A->bool`);
   ("inseg", `:(A#A->bool)->(A#A->bool)->bool`);
   ("woset", `:(A#A->bool)->bool`);
   ("chain", `:(A#A->bool)->(A->bool)->bool`);
   ("poset", `:(A#A->bool)->bool`); ("fl", `:(A#A->bool)->A->bool`);
   ("less", `:(A#A->bool)->A#A->bool`);
   ("angle", `:real^A#real^A#real^A->real`);
   ("vector_angle", `:real^A->real^A->real`); ("acs", `:real->real`);
   ("asn", `:real->real`); ("cacs", `:real^2->real^2`);
   ("casn", `:real^2->real^2`); ("atn", `:real->real`);
   ("catn", `:real^2->real^2`); ("unwinding", `:real^2->real^2`);
   ("cpow", `:real^2->real^2->real^2`); ("clog", `:real^2->real^2`);
   ("tan", `:real->real`); ("ctan", `:real^2->real^2`);
   ("rotate2d", `:real->real^2->real^2`); ("Arg", `:real^2->real`);
   ("pi", `:real`); ("log", `:real->real`); ("cos", `:real->real`);
   ("sin", `:real->real`); ("exp", `:real->real`);
   ("csin", `:real^2->real^2`); ("ccos", `:real^2->real^2`);
   ("cexp", `:real^2->real^2`);
   ("analytic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
   ("holomorphic_on", `:(real^2->real^2)->(real^2->bool)->bool`);
   ("higher_complex_derivative", `:num->(real^2->real^2)->real^2->real^2`);
   ("complex_derivative", `:(real^2->real^2)->real^2->real^2`);
   ("complex_differentiable", `:(real^2->real^2)->(real^2)net->bool`);
   ("has_complex_derivative", `:(real^2->real^2)->real^2->(real^2)net->bool`);
   ("cproduct", `:(A->bool)->(A->real^2)->real^2`);
   ("real", `:real^2->bool`); ("csqrt", `:real^2->real^2`);
   ("cnj", `:real^2->real^2`); ("complex_pow", `:real^2->num->real^2`);
   ("complex_div", `:real^2->real^2->real^2`);
   ("complex_inv", `:real^2->real^2`);
   ("complex_mul", `:real^2->real^2->real^2`); ("ii", `:real^2`);
   ("Cx", `:real->real^2`); ("complex", `:real#real->real^2`);
   ("Im", `:real^2->real`); ("Re", `:real^2->real`);
   ("absolutely_integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("negligible", `:(real^A->bool)->bool`);
   ("indicator", `:(real^M->bool)->real^M->real^1`);
   ("division_points",
    `:(real^N->bool)->((real^N->bool)->bool)->num#real->bool`);
   ("lifted", `:(A->A->B)->(A)option->(A)option->(B)option`);
   ("operative", `:(A->A->A)->((real^N->bool)->A)->bool`);
   ("integral", `:(real^A->bool)->(real^A->real^B)->real^B`);
   ("integrable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("has_integral", `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
   ("has_integral_compact_interval",
    `:(real^B->real^A)->real^A->(real^B->bool)->bool`);
   ("fine", `:(A->B->bool)->(A#(B->bool)->bool)->bool`);
   ("tagged_division_of",
    `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
   ("tagged_partial_division_of",
    `:(real^A#(real^A->bool)->bool)->(real^A->bool)->bool`);
   ("division_of", `:((real^A->bool)->bool)->(real^A->bool)->bool`);
   ("gauge", `:(real^A->real^A->bool)->bool`);
   ("content", `:(real^M->bool)->real`);
   ("interval_lowerbound", `:(real^M->bool)->real^M`);
   ("interval_upperbound", `:(real^M->bool)->real^M`);
   ("vector_derivative", `:(real^1->real^N)->(real^1)net->real^N`);
   ("has_vector_derivative", `:(real^1->real^A)->real^A->(real^1)net->bool`);
   ("jacobian", `:(real^A->real^B)->(real^A)net->real^A^B`);
   ("frechet_derivative", `:(real^A->real^B)->(real^A)net->real^A->real^B`);
   ("differentiable_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("differentiable", `:(real^B->real^A)->(real^B)net->bool`);
   ("has_derivative",
    `:(real^B->real^A)->(real^B->real^A)->(real^B)net->bool`);
   ("interval_bij", `:real^N#real^N->real^N#real^N->real^N->real^N`);
   ("retract_of", `:(real^A->bool)->(real^A->bool)->bool`);
   ("retraction", `:(real^N->bool)#(real^N->bool)->(real^N->real^N)->bool`);
   ("reduced", `:((num->num)->num->num)->num->(num->num)->num`);
   ("ksimplex", `:num->num->((num->num)->bool)->bool`);
   ("kle", `:num->(num->num)->(num->num)->bool`);
   ("path_connected", `:(real^A->bool)->bool`);
   ("path_component", `:(real^A->bool)->real^A->real^A->bool`);
   ("linepath", `:real^A#real^A->real^1->real^A`);
   ("shiftpath", `:real^1->(real^1->real^N)->real^1->real^N`);
   ("arc", `:(real^1->real^N)->bool`);
   ("simple_path", `:(real^1->real^N)->bool`);
   ("++", `:(real^1->A)->(real^1->A)->real^1->A`);
   ("reversepath", `:(real^1->real^N)->real^1->real^N`);
   ("path_image", `:(real^1->real^N)->real^N->bool`);
   ("pathfinish", `:(real^1->real^N)->real^N`);
   ("pathstart", `:(real^1->real^N)->real^N`);
   ("path", `:(real^1->real^N)->bool`);
   ("extreme_point_of", `:real^A->(real^A->bool)->bool`);
   ("face_of", `:(real^A->bool)->(real^A->bool)->bool`);
   ("relative_interior", `:(real^A->bool)->real^A->bool`);
   ("starlike", `:(real^A->bool)->bool`);
   ("epigraph",
    `:(real^N->bool)->(real^N->real)->real^(N,1)finite_sum->bool`);
   ("convex_on", `:(real^A->real)->(real^A->bool)->bool`);
   ("coplanar", `:(real^A->bool)->bool`);
   ("affine_dependent", `:(real^N->bool)->bool`);
   ("conic", `:(real^A->bool)->bool`); ("convex", `:(real^A->bool)->bool`);
   ("affine", `:(real^A->bool)->bool`);
   ("closest_point", `:(real^A->bool)->real^A->real^A`);
   ("from", `:num->num->bool`);
   ("summable", `:(num->bool)->(num->real^A)->bool`);
   ("infsum", `:(num->bool)->(num->real^A)->real^A`);
   ("sums", `:(num->real^A)->real^A->(num->bool)->bool`);
   ("homeomorphic", `:(real^A->bool)->(real^B->bool)->bool`);
   ("homeomorphism",
    `:(real^B->bool)#(real^A->bool)->(real^B->real^A)#(real^A->real^B)->bool`);
   ("open_segment", `:real^A#real^A->real^A->bool`);
   ("closed_segment", `:(real^A#real^A)list->real^A->bool`);
   ("is_interval", `:(real^N->bool)->bool`);
   ("closed_interval", `:(real^N#real^N)list->real^N->bool`);
   ("open_interval", `:real^N#real^N->real^N->bool`);
   ("diameter", `:(real^A->bool)->real`);
   ("connected_component", `:(real^A->bool)->real^A->real^A->bool`);
   ("uniformly_continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("continuous_on", `:(real^B->real^A)->(real^B->bool)->bool`);
   ("continuous", `:(B->real^A)->(B)net->bool`);
   ("complete", `:(real^N->bool)->bool`); ("cauchy", `:(num->real^N)->bool`);
   ("compact", `:(real^N->bool)->bool`);
   ("bounded", `:(real^N->bool)->bool`); ("netlimit", `:(A)net->A`);
   ("lim", `:(A)net->(A->real^B)->real^B`);
   ("-->", `:(B->real^A)->real^A->(B)net->bool`);
   ("eventually", `:(A->bool)->(A)net->bool`);
   ("trivial_limit", `:(A)net->bool`);
   ("in_direction", `:real^A->real^A->(real^A)net`);
   ("within", `:(A)net->(A->bool)->(A)net`); ("sequentially", `:(num)net`);
   ("at_infinity", `:(real^A)net`); ("at", `:real^A->(real^A)net`);
   ("netord", `:(A)net->A->A->bool`); ("mk_net", `:(A->A->bool)->(A)net`);
   ("frontier", `:(real^A->bool)->real^A->bool`);
   ("closure", `:(real^A->bool)->real^A->bool`);
   ("interior", `:(real^A->bool)->real^A->bool`);
   ("limit_point_of", `:real^A->(real^A->bool)->bool`);
   ("connected", `:(real^A->bool)->bool`);
   ("cball", `:real^A#real->real^A->bool`);
   ("ball", `:real^A#real->real^A->bool`);
   ("euclidean", `:(real^A)topology`); ("closed", `:(real^N->bool)->bool`);
   ("open", `:(real^A->bool)->bool`);
   ("subtopology", `:(A)topology->(A->bool)->(A)topology`);
   ("closed_in", `:(A)topology->(A->bool)->bool`);
   ("topspace", `:(A)topology->A->bool`);
   ("open_in", `:(A)topology->(A->bool)->bool`);
   ("topology", `:((A->bool)->bool)->(A)topology`);
   ("istopology", `:((A->bool)->bool)->bool`);
   ("ITER", `:num->(A->A)->A->A`); ("frac", `:real->real`);
   ("floor", `:real->real`); ("integer", `:real->bool`);
   ("cross", `:real^3->real^3->real^3`);
   ("rotoinversion_matrix", `:real^A^A->bool`);
   ("rotation_matrix", `:real^A^A->bool`);
   ("orthogonal_matrix", `:real^N^N->bool`);
   ("orthogonal_transformation", `:(real^N->real^N)->bool`);
   ("det", `:real^N^N->real`); ("trace", `:real^N^N->real`);
   ("product", `:(A->bool)->(A->real)->real`); ("sign", `:(A->A)->real`);
   ("evenperm", `:(A->A)->bool`); ("permutation", `:(A->A)->bool`);
   ("swapseq", `:num->(A->A)->bool`); ("swap", `:A#A->A->A`);
   ("inverse", `:(B->A)->A->B`); ("permutes", `:(A->A)->(A->bool)->bool`);
   ("midpoint", `:real^A#real^A->real^A`);
   ("between", `:real^A->real^A#real^A->bool`);
   ("collinear", `:(real^A->bool)->bool`); ("infnorm", `:real^N->real`);
   ("rank", `:real^M^N->num`); ("columnvector", `:real^N->real^1^N`);
   ("rowvector", `:real^N->real^N^1`); ("dim", `:(real^A->bool)->num`);
   ("independent", `:(real^A->bool)->bool`);
   ("dependent", `:(real^A->bool)->bool`);
   ("span", `:(real^A->bool)->real^A->bool`);
   ("subspace", `:(real^A->bool)->bool`); ("drop", `:real^1->real`);
   ("lift", `:real->real^1`); ("onorm", `:(real^M->real^N)->real`);
   ("matrix", `:(real^M->real^N)->real^M^N`);
   ("matrix_inv", `:real^N^M->real^M^N`); ("invertible", `:real^N^M->bool`);
   ("columns", `:real^N^M->real^M->bool`);
   ("rows", `:real^N^M->real^N->bool`); ("column", `:num->real^N^M->real^M`);
   ("row", `:num->real^N^M->real^N`); ("transp", `:real^N^M->real^M^N`);
   ("mat", `:num->real^N^M`);
   ("vector_matrix_mul", `:real^M->real^N^M->real^N`);
   ("matrix_vector_mul", `:real^N^M->real^N->real^M`);
   ("matrix_mul", `:real^N^M->real^P^N->real^P^M`);
   ("matrix_sub", `:real^N^M->real^N^M->real^N^M`);
   ("matrix_add", `:real^N^M->real^N^M->real^N^M`);
   ("matrix_neg", `:real^N^M->real^N^M`);
   ("adjoint", `:(real^M->real^N)->real^N->real^M`);
   ("bilinear", `:(real^A->real^B->real^C)->bool`);
   ("linear", `:(real^M->real^N)->bool`);
   ("orthogonal", `:real^A->real^A->bool`); ("basis", `:num->real^A`);
   ("vsum", `:(A->bool)->(A->real^N)->real^N`);
   ("distance", `:real^A#real^A->real`); ("vector_norm", `:real^A->real`);
   ("dot", `:real^N->real^N->real`); ("vec", `:num->real^N`);
   ("%", `:real->real^N->real^N`); ("vector_neg", `:real^N->real^N`);
   ("vector_sub", `:real^N->real^N->real^N`);
   ("vector_add", `:real^N->real^N->real^N`); ("sqrt", `:real->real`);
   ("hull", `:((A->bool)->bool)->(A->bool)->A->bool`);
   ("inf", `:(real->bool)->real`); ("sup", `:(real->bool)->real`);
   ("superadmissible",
    `:(A->A->bool)->((A->C)->B->bool)->(B->A)->((A->C)->B->C)->bool`);
   ("tailadmissible",
    `:(A->A->bool)->((A->B)->P->bool)->(P->A)->((A->B)->P->B)->bool`);
   ("admissible",
    `:(B->A->bool)->((B->C)->D->bool)->(D->A)->((B->C)->D->E)->bool`);
   ("CASEWISE", `:((A->C)#(B->A->D))list->B->C->D`);
   ("vector", `:(A)list->A^N`);
   ("dest_auto_define_finite_type_3", `:3->num`);
   ("mk_auto_define_finite_type_3", `:num->3`);
   ("dest_auto_define_finite_type_2", `:2->num`);
   ("mk_auto_define_finite_type_2", `:num->2`);
   ("sndcart", `:A^(M,N)finite_sum->A^N`);
   ("fstcart", `:A^(M,N)finite_sum->A^M`);
   ("pastecart", `:A^M->A^N->A^(M,N)finite_sum`);
   ("dest_finite_sum", `:(A,B)finite_sum->num`);
   ("mk_finite_sum", `:num->(A,B)finite_sum`); ("lambda", `:(num->A)->A^B`);
   ("$", `:B^A->num->B`); ("dest_cart", `:A^B->(B)finite_image->A`);
   ("mk_cart", `:((B)finite_image->A)->A^B`);
   ("dest_finite_image", `:(A)finite_image->num`);
   ("finite_index", `:num->(A)finite_image`);
   ("dimindex", `:(A->bool)->num`); ("sum", `:(A->bool)->(A->real)->real`);
   ("nsum", `:(A->bool)->(A->num)->num`);
   ("iterate", `:(B->B->B)->(A->bool)->(A->B)->B`);
   ("support", `:(B->B->B)->(A->B)->(A->bool)->A->bool`);
   ("monoidal", `:(A->A->A)->bool`); ("neutral", `:(A->A->A)->A`);
   ("..", `:num->num->num->bool`); ("COUNTABLE", `:(A->bool)->bool`);
   (">_c", `:(A->bool)->(B->bool)->bool`);
   (">=_c", `:(A->bool)->(B->bool)->bool`);
   ("=_c", `:(A->bool)->(B->bool)->bool`);
   ("<_c", `:(A->bool)->(B->bool)->bool`);
   ("<=_c", `:(A->bool)->(B->bool)->bool`);
   ("PAIRWISE", `:(A->A->bool)->(A)list->bool`);
   ("pairwise", `:(A->A->bool)->(A->bool)->bool`);
   ("list_of_set", `:(A->bool)->(A)list`);
   ("set_of_list", `:(A)list->A->bool`);
   ("CROSS", `:(A->bool)->(B->bool)->A#B->bool`);
   ("HAS_SIZE", `:(A->bool)->num->bool`); ("CARD", `:(A->bool)->num`);
   ("ITSET", `:(A->B->B)->(A->bool)->B->B`);
   ("FINREC", `:(A->B->B)->B->(A->bool)->B->num->bool`);
   ("REST", `:(A->bool)->A->bool`); ("CHOICE", `:(A->bool)->A`);
   ("BIJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
   ("SURJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
   ("INJ", `:(A->B)->(A->bool)->(B->bool)->bool`);
   ("IMAGE", `:(A->B)->(A->bool)->B->bool`);
   ("INFINITE", `:(A->bool)->bool`); ("FINITE", `:(A->bool)->bool`);
   ("SING", `:(A->bool)->bool`); ("DISJOINT", `:(A->bool)->(A->bool)->bool`);
   ("PSUBSET", `:(A->bool)->(A->bool)->bool`);
   ("SUBSET", `:(A->bool)->(A->bool)->bool`);
   ("DELETE", `:(A->bool)->A->A->bool`);
   ("DIFF", `:(A->bool)->(A->bool)->A->bool`);
   ("INTERS", `:((A->bool)->bool)->A->bool`);
   ("INTER", `:(A->bool)->(A->bool)->A->bool`);
   ("UNIONS", `:((A->bool)->bool)->A->bool`);
   ("UNION", `:(A->bool)->(A->bool)->A->bool`); ("UNIV", `:A->bool`);
   ("INSERT", `:A->(A->bool)->A->bool`); ("EMPTY", `:A->bool`);
   ("SETSPEC", `:A->bool->A->bool`); ("GSPEC", `:(A->bool)->A->bool`);
   ("IN", `:A->(A->bool)->bool`); ("num_gcd", `:num#num->num`);
   ("num_coprime", `:num#num->bool`); ("num_mod", `:num->num->num->bool`);
   ("num_divides", `:num->num->bool`); ("num_of_int", `:int->num`);
   ("int_gcd", `:int#int->int`); ("int_coprime", `:int#int->bool`);
   ("int_mod", `:int->int->int->bool`); ("int_divides", `:int->int->bool`);
   ("real_mod", `:real->real->real->bool`);
   ("==", `:A->A->(A->A->bool)->bool`); ("rem", `:int->int->int`);
   ("div", `:int->int->int`); ("int_pow", `:int->num->int`);
   ("int_min", `:int->int->int`); ("int_max", `:int->int->int`);
   ("int_abs", `:int->int`); ("int_mul", `:int->int->int`);
   ("int_sub", `:int->int->int`); ("int_add", `:int->int->int`);
   ("int_neg", `:int->int`); ("int_of_num", `:num->int`);
   ("int_gt", `:int->int->bool`); ("int_ge", `:int->int->bool`);
   ("int_lt", `:int->int->bool`); ("int_le", `:int->int->bool`);
   ("real_of_int", `:int->real`); ("int_of_real", `:real->int`);
   ("is_int", `:real->bool`); ("DECIMAL", `:num->num->real`);
   ("real_min", `:real->real->real`); ("real_max", `:real->real->real`);
   ("real_div", `:real->real->real`); ("real_pow", `:real->num->real`);
   ("real_abs", `:real->real`); ("real_gt", `:real->real->bool`);
   ("real_ge", `:real->real->bool`); ("real_lt", `:real->real->bool`);
   ("real_sub", `:real->real->real`); ("real_inv", `:real->real`);
   ("real_le", `:real->real->bool`); ("real_mul", `:real->real->real`);
   ("real_add", `:real->real->real`); ("real_neg", `:real->real`);
   ("real_of_num", `:num->real`); ("dest_real", `:real->hreal#hreal->bool`);
   ("mk_real", `:(hreal#hreal->bool)->real`);
   ("treal_eq", `:hreal#hreal->hreal#hreal->bool`);
   ("treal_inv", `:hreal#hreal->hreal#hreal`);
   ("treal_le", `:hreal#hreal->hreal#hreal->bool`);
   ("treal_mul", `:hreal#hreal->hreal#hreal->hreal#hreal`);
   ("treal_add", `:hreal#hreal->hreal#hreal->hreal#hreal`);
   ("treal_neg", `:hreal#hreal->hreal#hreal`);
   ("treal_of_num", `:num->hreal#hreal`); ("hreal_inv", `:hreal->hreal`);
   ("hreal_le", `:hreal->hreal->bool`);
   ("hreal_mul", `:hreal->hreal->hreal`);
   ("hreal_add", `:hreal->hreal->hreal`); ("hreal_of_num", `:num->hreal`);
   ("dest_hreal", `:hreal->nadd->bool`);
   ("mk_hreal", `:(nadd->bool)->hreal`); ("nadd_inv", `:nadd->nadd`);
   ("nadd_rinv", `:nadd->num->num`); ("nadd_mul", `:nadd->nadd->nadd`);
   ("nadd_add", `:nadd->nadd->nadd`); ("nadd_le", `:nadd->nadd->bool`);
   ("nadd_of_num", `:num->nadd`); ("nadd_eq", `:nadd->nadd->bool`);
   ("dest_nadd", `:nadd->num->num`); ("mk_nadd", `:(num->num)->nadd`);
   ("is_nadd", `:(num->num)->bool`); ("dist", `:num#num->num`);
   ("ASCII", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
   ("_16756", `:bool->bool->bool->bool->bool->bool->bool->bool->char`);
   ("_dest_char", `:char->(bool#bool#bool#bool#bool#bool#bool#bool)recspace`);
   ("_mk_char", `:(bool#bool#bool#bool#bool#bool#bool#bool)recspace->char`);
   ("ZIP", `:(A)list->(B)list->(A#B)list`);
   ("ITLIST2", `:(A->B->C->C)->(A)list->(B)list->C->C`);
   ("ASSOC", `:A->(A#B)list->B`); ("FILTER", `:(A->bool)->(A)list->(A)list`);
   ("EL", `:num->(A)list->A`);
   ("MAP2", `:(A->B->C)->(A)list->(B)list->(C)list`);
   ("ALL2", `:(A->B->bool)->(A)list->(B)list->bool`);
   ("MEM", `:A->(A)list->bool`); ("ITLIST", `:(A->B->B)->(A)list->B->B`);
   ("EX", `:(A->bool)->(A)list->bool`); ("ALL", `:(A->bool)->(A)list->bool`);
   ("NULL", `:(A)list->bool`); ("REPLICATE", `:num->A->(A)list`);
   ("LAST", `:(A)list->A`); ("MAP", `:(A->B)->(A)list->(B)list`);
   ("LENGTH", `:(A)list->num`); ("REVERSE", `:(A)list->(A)list`);
   ("APPEND", `:(A)list->(A)list->(A)list`); ("TL", `:(A)list->(A)list`);
   ("HD", `:(A)list->A`); ("ISO", `:(A->B)->(B->A)->bool`);
   ("CONS", `:A->(A)list->(A)list`); ("NIL", `:(A)list`);
   ("_dest_list", `:(A)list->(A)recspace`);
   ("_mk_list", `:(A)recspace->(A)list`); ("SOME", `:A->(A)option`);
   ("NONE", `:(A)option`); ("_dest_option", `:(A)option->(A)recspace`);
   ("_mk_option", `:(A)recspace->(A)option`); ("OUTR", `:A+B->B`);
   ("OUTL", `:A+B->A`); ("INR", `:B->A+B`); ("INL", `:A->A+B`);
   ("_dest_sum", `:A+B->(A#B)recspace`); ("_mk_sum", `:(A#B)recspace->A+B`);
   ("FNIL", `:num->A`); ("FCONS", `:A->(num->A)->num->A`);
   ("CONSTR", `:num->A->(num->(A)recspace)->(A)recspace`);
   ("BOTTOM", `:(A)recspace`); ("_dest_rec", `:(A)recspace->num->A->bool`);
   ("_mk_rec", `:(num->A->bool)->(A)recspace`);
   ("ZRECSPACE", `:(num->A->bool)->bool`); ("ZBOT", `:num->A->bool`);
   ("ZCONSTR", `:num->A->(num->num->A->bool)->num->A->bool`);
   ("INJP", `:(num->A->bool)->(num->A->bool)->num->A->bool`);
   ("INJF", `:(num->num->A->bool)->num->A->bool`);
   ("INJA", `:A->num->A->bool`); ("INJN", `:num->num->A->bool`);
   ("NUMRIGHT", `:num->num`); ("NUMLEFT", `:num->bool`);
   ("NUMSUM", `:bool->num->num`); ("NUMSND", `:num->num`);
   ("NUMFST", `:num->num`); ("NUMPAIR", `:num->num->num`);
   ("MEASURE", `:(A->num)->A->A->bool`); ("WF", `:(A->A->bool)->bool`);
   ("minimal", `:(num->bool)->num`); ("MIN", `:num->num->num`);
   ("MAX", `:num->num->num`); ("MOD", `:num->num->num`);
   ("DIV", `:num->num->num`); ("FACT", `:num->num`); ("-", `:num->num->num`);
   ("ODD", `:num->bool`); ("EVEN", `:num->bool`); (">", `:num->num->bool`);
   (">=", `:num->num->bool`); ("<", `:num->num->bool`);
   ("<=", `:num->num->bool`); ("EXP", `:num->num->num`);
   ("*", `:num->num->num`); ("BIT1", `:num->num`); ("BIT0", `:num->num`);
   ("+", `:num->num->num`); ("PRE", `:num->num`); ("NUMERAL", `:num->num`);
   ("SUC", `:num->num`); ("_0", `:num`); ("dest_num", `:num->ind`);
   ("mk_num", `:ind->num`); ("NUM_REP", `:ind->bool`); ("IND_0", `:ind`);
   ("IND_SUC", `:ind->ind`); ("ONTO", `:(A->B)->bool`);
   ("ONE_ONE", `:(A->B)->bool`); ("PASSOC", `:((A#B)#C->D)->A#B#C->D`);
   ("UNCURRY", `:(A->B->C)->A#B->C`); ("CURRY", `:(A#B->C)->A->B->C`);
   ("SND", `:A#B->B`); ("FST", `:A#B->A`); (",", `:A->B->A#B`);
   ("REP_prod", `:A#B->A->B->bool`); ("ABS_prod", `:(A->B->bool)->A#B`);
   ("mk_pair", `:A->B->A->B->bool`); ("_FUNCTION", `:(A->B->bool)->A->B`);
   ("_MATCH", `:A->(A->B->bool)->B`);
   ("_GUARDED_PATTERN", `:bool->bool->bool->bool`);
   ("_UNGUARDED_PATTERN", `:bool->bool->bool`);
   ("_SEQPATTERN", `:(A->B->bool)->(A->B->bool)->A->B->bool`);
   ("GEQ", `:A->A->bool`); ("GABS", `:(A->bool)->A`); ("LET_END", `:A->A`);
   ("LET", `:(A->B)->A->B`); ("one", `:1`); ("one_REP", `:1->bool`);
   ("one_ABS", `:bool->1`); ("I", `:A->A`); ("o", `:(B->C)->(A->B)->A->C`);
   ("COND", `:bool->A->A->A`); ("@", `:(A->bool)->A`);
   ("_FALSITY_", `:bool`); ("?!", `:(A->bool)->bool`); ("~", `:bool->bool`);
   ("F", `:bool`); ("\\/", `:bool->bool->bool`); ("?", `:(A->bool)->bool`);
   ("!", `:(A->bool)->bool`); ("==>", `:bool->bool->bool`);
   ("/\\", `:bool->bool->bool`); ("T", `:bool`); ("=", `:A->A->bool`)];;

  let the_loaded_files =  ["flyspeck.ml"; "wlog_examples.ml"; "wlog.ml"; "real.ml"; "measure.ml";
   "card.ml"; "wo.ml"; "geom.ml"; "transc.ml"; "canal.ml"; "complex.ml";
   "integration.ml"; "analysis.ml"; "dimension.ml"; "convex.ml";
   "topology.ml"; "iter.ml"; "floor.ml"; "cross.ml"; "determinants.ml";
   "products.ml"; "permutations.ml"; "vectors.ml"; "misc.ml"; "database.ml";
   "help.ml"; "define.ml"; "cart.ml"; "iter.ml"; "sets.ml"; "int.ml";
   "calc_rat.ml"; "real.ml"; "realarith.ml"; "calc_int.ml"; "realax.ml";
   "list.ml"; "ind-types.ml"; "grobner.ml"; "normalizer.ml"; "calc_num.ml";
   "wf.ml"; "arith.ml"; "num.ml"; "pair.ml"; "recursion.ml"; "quot.ml";
   "meson.ml"; "canon.ml"; "trivia.ml"; "class.ml"; "ind-defs.ml";
   "theorems.ml"; "simp.ml"; "itab.ml"; "tactics.ml"; "drule.ml"; "bool.ml";
   "equal.ml"; "printer.ml"; "parser.ml"; "preterm.ml"; "nets.ml";
   "basics.ml"; "fusion.ml"; "lib.ml"; "sys.ml"];;

  let the_overload_skeletons = [("real_interval", `:A`); ("segment", `:A`); ("interval", `:A`);
   ("**", `:A->B->C`); ("norm", `:A->real`); ("gcd", `:A#A->A`);
   ("coprime", `:A#A->bool`); ("mod", `:A->A->A->bool`);
   ("divides", `:A->A->bool`); ("&", `:num->A`); ("min", `:A->A->A`);
   ("max", `:A->A->A`); ("abs", `:A->A`); ("inv", `:A->A`);
   ("pow", `:A->num->A`); ("--", `:A->A`); (">=", `:A->A->bool`);
   (">", `:A->A->bool`); ("<=", `:A->A->bool`); ("<", `:A->A->bool`);
   ("/", `:A->A->A`); ("*", `:A->A->A`); ("-", `:A->A->A`);
   ("+", `:A->A->A`)];;

  let the_interface =   [("vol", ("measure", `:(real^3->bool)->real`));
   ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
   ("+", ("vector_add", `:real^N->real^N->real^N`));
   ("-", ("vector_sub", `:real^N->real^N->real^N`));
   ("--", ("vector_neg", `:real^N->real^N`));
   ("norm", ("vector_norm", `:real^N->real`));
   ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
   ("real_interval",
    ("closed_real_interval", `:(real#real)list->real->bool`));
   ("real_interval", ("open_real_interval", `:real#real->real->bool`));
   ("+", ("real_add", `:real->real->real`));
   ("-", ("real_sub", `:real->real->real`));
   ("*", ("real_mul", `:real->real->real`));
   ("/", ("real_div", `:real->real->real`));
   ("<", ("real_lt", `:real->real->bool`));
   ("<=", ("real_le", `:real->real->bool`));
   (">", ("real_gt", `:real->real->bool`));
   (">=", ("real_ge", `:real->real->bool`));
   ("--", ("real_neg", `:real->real`));
   ("pow", ("real_pow", `:real->num->real`));
   ("inv", ("real_inv", `:real->real`));
   ("abs", ("real_abs", `:real->real`));
   ("max", ("real_max", `:real->real->real`));
   ("min", ("real_min", `:real->real->real`));
   ("&", ("real_of_num", `:num->real`));
   ("mod", ("real_mod", `:real->real->real->bool`));
   ("inv", ("complex_inv", `:real^2->real^2`));
   ("pow", ("complex_pow", `:real^2->num->real^2`));
   ("/", ("complex_div", `:real^2->real^2->real^2`));
   ("*", ("complex_mul", `:real^2->real^2->real^2`));
   ("-", ("vector_sub", `:real^2->real^2->real^2`));
   ("+", ("vector_add", `:real^2->real^2->real^2`));
   ("--", ("vector_neg", `:real^2->real^2`));
   ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
   ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
   ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
   ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
   ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
   ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
   ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
   ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
   ("--", ("matrix_neg", `:real^N^M->real^N^M`));
   ("dist", ("distance", `:real^N#real^N->real`));
   ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
   ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
   ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
   (">=", (">=", `:num->num->bool`));
   ("divides", ("num_divides", `:num->num->bool`));
   ("mod", ("num_mod", `:num->num->num->bool`));
   ("coprime", ("num_coprime", `:num#num->bool`));
   ("gcd", ("num_gcd", `:num#num->num`));
   ("gcd", ("int_gcd", `:int#int->int`));
   ("coprime", ("int_coprime", `:int#int->bool`));
   ("mod", ("int_mod", `:int->int->int->bool`));
   ("divides", ("int_divides", `:int->int->bool`));
   ("&", ("int_of_num", `:num->int`));
   ("min", ("int_min", `:int->int->int`));
   ("max", ("int_max", `:int->int->int`)); ("abs", ("int_abs", `:int->int`));
   ("pow", ("int_pow", `:int->num->int`)); ("--", ("int_neg", `:int->int`));
   (">=", ("int_ge", `:int->int->bool`));
   (">", ("int_gt", `:int->int->bool`));
   ("<=", ("int_le", `:int->int->bool`));
   ("<", ("int_lt", `:int->int->bool`));
   ("*", ("int_mul", `:int->int->int`));
   ("-", ("int_sub", `:int->int->int`));
   ("+", ("int_add", `:int->int->int`));
   ("&", ("hreal_of_num", `:num->hreal`));
   ("<=>", ("=", `:bool->bool->bool`))];;

  let the_types = [("net", 1); ("topology", 1); ("3", 0); ("2", 0); ("finite_sum", 2);
   ("cart", 2); ("finite_image", 1); ("int", 0); ("real", 0); ("hreal", 0);
   ("nadd", 0); ("char", 0); ("list", 1); ("option", 1); ("sum", 2);
   ("recspace", 1); ("num", 0); ("ind", 0); ("prod", 2); ("1", 0);
   ("bool", 0); ("fun", 2)];;
  
end;;

module Snapshot_flyspeck_init_2010_02_11 : Snapshot_type = struct

  let the_constants = Snapshot_v220_7_31_2009.the_constants;;
  let the_loaded_files = Snapshot_v220_7_31_2009.the_loaded_files;;
  let the_types = Snapshot_v220_7_31_2009.the_types;;
  let the_overload_skeletons = Snapshot_v220_7_31_2009.the_overload_skeletons;;

(*

(* start with the hol-light snapshot v220_7_31_2009 then  *)
prioritize_complex();; (* lowest priority *)
prioritize_int();;
prioritize_num();;
prioritize_vector();;
prioritize_real();;  (* highest priority *)

*)

  let the_interface = 
  [("+", ("real_add", `:real->real->real`));
   ("-", ("real_sub", `:real->real->real`));
   ("*", ("real_mul", `:real->real->real`));
   ("/", ("real_div", `:real->real->real`));
   ("<", ("real_lt", `:real->real->bool`));
   ("<=", ("real_le", `:real->real->bool`));
   (">", ("real_gt", `:real->real->bool`));
   (">=", ("real_ge", `:real->real->bool`));
   ("--", ("real_neg", `:real->real`));
   ("pow", ("real_pow", `:real->num->real`));
   ("inv", ("real_inv", `:real->real`));
   ("abs", ("real_abs", `:real->real`));
   ("max", ("real_max", `:real->real->real`));
   ("min", ("real_min", `:real->real->real`));
   ("&", ("real_of_num", `:num->real`));
   ("mod", ("real_mod", `:real->real->real->bool`));
   ("+", ("vector_add", `:real^N->real^N->real^N`));
   ("-", ("vector_sub", `:real^N->real^N->real^N`));
   ("--", ("vector_neg", `:real^N->real^N`));
   ("norm", ("vector_norm", `:real^N->real`));
   ("**", ("vector_matrix_mul", `:real^M->real^N^M->real^N`));
   ("+", ("+", `:num->num->num`)); ("-", ("-", `:num->num->num`));
   ("*", ("*", `:num->num->num`)); ("<", ("<", `:num->num->bool`));
   ("<=", ("<=", `:num->num->bool`)); (">", (">", `:num->num->bool`));
   (">=", (">=", `:num->num->bool`));
   ("divides", ("num_divides", `:num->num->bool`));
   ("mod", ("num_mod", `:num->num->num->bool`));
   ("coprime", ("num_coprime", `:num#num->bool`));
   ("gcd", ("num_gcd", `:num#num->num`));
   ("+", ("int_add", `:int->int->int`));
   ("-", ("int_sub", `:int->int->int`));
   ("*", ("int_mul", `:int->int->int`));
   ("<", ("int_lt", `:int->int->bool`));
   ("<=", ("int_le", `:int->int->bool`));
   (">", ("int_gt", `:int->int->bool`));
   (">=", ("int_ge", `:int->int->bool`)); ("--", ("int_neg", `:int->int`));
   ("pow", ("int_pow", `:int->num->int`)); ("abs", ("int_abs", `:int->int`));
   ("max", ("int_max", `:int->int->int`));
   ("min", ("int_min", `:int->int->int`));
   ("&", ("int_of_num", `:num->int`));
   ("divides", ("int_divides", `:int->int->bool`));
   ("mod", ("int_mod", `:int->int->int->bool`));
   ("coprime", ("int_coprime", `:int#int->bool`));
   ("gcd", ("int_gcd", `:int#int->int`));
   ("inv", ("complex_inv", `:real^2->real^2`));
   ("pow", ("complex_pow", `:real^2->num->real^2`));
   ("/", ("complex_div", `:real^2->real^2->real^2`));
   ("*", ("complex_mul", `:real^2->real^2->real^2`));
   ("-", ("vector_sub", `:real^2->real^2->real^2`));
   ("+", ("vector_add", `:real^2->real^2->real^2`));
   ("--", ("vector_neg", `:real^2->real^2`));
   ("vol", ("measure", `:(real^3->bool)->real`));
   ("NULLSET", ("negligible", `:(real^3->bool)->bool`));
   ("real_interval",
    ("closed_real_interval", `:(real#real)list->real->bool`));
   ("real_interval", ("open_real_interval", `:real#real->real->bool`));
   ("segment", ("closed_segment", `:(real^A#real^A)list->real^A->bool`));
   ("segment", ("open_segment", `:real^A#real^A->real^A->bool`));
   ("interval", ("closed_interval", `:(real^A#real^A)list->real^A->bool`));
   ("interval", ("open_interval", `:real^A#real^A->real^A->bool`));
   ("**", ("matrix_vector_mul", `:real^N^M->real^N->real^M`));
   ("**", ("matrix_mul", `:real^N^M->real^P^N->real^P^M`));
   ("-", ("matrix_sub", `:real^N^M->real^N^M->real^N^M`));
   ("+", ("matrix_add", `:real^N^M->real^N^M->real^N^M`));
   ("--", ("matrix_neg", `:real^N^M->real^N^M`));
   ("dist", ("distance", `:real^N#real^N->real`));
   ("&", ("hreal_of_num", `:num->hreal`));
   ("<=>", ("=", `:bool->bool->bool`))];;

 end;;