extracted/setoids.ml

   1 open Preamble
   2
   3 open Core_notation
   4
   5 open Pts
   6
   7 open Hints_declaration
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Relations
  14
  15 type setoid =
  16 | Mk_Setoid
  17
  18 (** val setoid_rect_Type4 :
  19     (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
  20 let rec setoid_rect_Type4 h_mk_Setoid = function
  21 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
  22
  23 (** val setoid_rect_Type5 :
  24     (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
  25 let rec setoid_rect_Type5 h_mk_Setoid = function
  26 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
  27
  28 (** val setoid_rect_Type3 :
  29     (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
  30 let rec setoid_rect_Type3 h_mk_Setoid = function
  31 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
  32
  33 (** val setoid_rect_Type2 :
  34     (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
  35 let rec setoid_rect_Type2 h_mk_Setoid = function
  36 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
  37
  38 (** val setoid_rect_Type1 :
  39     (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
  40 let rec setoid_rect_Type1 h_mk_Setoid = function
  41 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
  42
  43 (** val setoid_rect_Type0 :
  44     (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
  45 let rec setoid_rect_Type0 h_mk_Setoid = function
  46 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
  47
  48 type std_supp = __
  49
  50 (** val setoid_inv_rect_Type4 :
  51     setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
  52 let setoid_inv_rect_Type4 hterm h1 =
  53   let hcut = setoid_rect_Type4 h1 hterm in hcut __
  54
  55 (** val setoid_inv_rect_Type3 :
  56     setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
  57 let setoid_inv_rect_Type3 hterm h1 =
  58   let hcut = setoid_rect_Type3 h1 hterm in hcut __
  59
  60 (** val setoid_inv_rect_Type2 :
  61     setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
  62 let setoid_inv_rect_Type2 hterm h1 =
  63   let hcut = setoid_rect_Type2 h1 hterm in hcut __
  64
  65 (** val setoid_inv_rect_Type1 :
  66     setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
  67 let setoid_inv_rect_Type1 hterm h1 =
  68   let hcut = setoid_rect_Type1 h1 hterm in hcut __
  69
  70 (** val setoid_inv_rect_Type0 :
  71     setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
  72 let setoid_inv_rect_Type0 hterm h1 =
  73   let hcut = setoid_rect_Type0 h1 hterm in hcut __
  74
  75 (** val as_std : setoid **)
  76 let as_std =
  77   Mk_Setoid
  78
  79 (** val std_prod : setoid -> setoid -> setoid **)
  80 let std_prod x y =
  81   Mk_Setoid
  82
  83 (** val std_union : setoid -> setoid -> setoid **)
  84 let std_union x y =
  85   Mk_Setoid
  86