extracted/deqsets.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Relations
  14
  15 open Bool
  16
  17 type deqSet =
  18   __ -> __ -> Bool.bool
  19   (* singleton inductive, whose constructor was mk_DeqSet *)
  20
  21 (** val deqSet_rect_Type4 :
  22     (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
  23 let rec deqSet_rect_Type4 h_mk_DeqSet x_3369 =
  24   let eqb = x_3369 in h_mk_DeqSet __ eqb __
  25
  26 (** val deqSet_rect_Type5 :
  27     (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
  28 let rec deqSet_rect_Type5 h_mk_DeqSet x_3371 =
  29   let eqb = x_3371 in h_mk_DeqSet __ eqb __
  30
  31 (** val deqSet_rect_Type3 :
  32     (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
  33 let rec deqSet_rect_Type3 h_mk_DeqSet x_3373 =
  34   let eqb = x_3373 in h_mk_DeqSet __ eqb __
  35
  36 (** val deqSet_rect_Type2 :
  37     (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
  38 let rec deqSet_rect_Type2 h_mk_DeqSet x_3375 =
  39   let eqb = x_3375 in h_mk_DeqSet __ eqb __
  40
  41 (** val deqSet_rect_Type1 :
  42     (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
  43 let rec deqSet_rect_Type1 h_mk_DeqSet x_3377 =
  44   let eqb = x_3377 in h_mk_DeqSet __ eqb __
  45
  46 (** val deqSet_rect_Type0 :
  47     (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
  48 let rec deqSet_rect_Type0 h_mk_DeqSet x_3379 =
  49   let eqb = x_3379 in h_mk_DeqSet __ eqb __
  50
  51 type carr = __
  52
  53 (** val eqb : deqSet -> __ -> __ -> Bool.bool **)
  54 let rec eqb xxx =
  55   let yyy = xxx in yyy
  56
  57 (** val deqSet_inv_rect_Type4 :
  58     deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
  59 let deqSet_inv_rect_Type4 hterm h1 =
  60   let hcut = deqSet_rect_Type4 h1 hterm in hcut __
  61
  62 (** val deqSet_inv_rect_Type3 :
  63     deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
  64 let deqSet_inv_rect_Type3 hterm h1 =
  65   let hcut = deqSet_rect_Type3 h1 hterm in hcut __
  66
  67 (** val deqSet_inv_rect_Type2 :
  68     deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
  69 let deqSet_inv_rect_Type2 hterm h1 =
  70   let hcut = deqSet_rect_Type2 h1 hterm in hcut __
  71
  72 (** val deqSet_inv_rect_Type1 :
  73     deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
  74 let deqSet_inv_rect_Type1 hterm h1 =
  75   let hcut = deqSet_rect_Type1 h1 hterm in hcut __
  76
  77 (** val deqSet_inv_rect_Type0 :
  78     deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
  79 let deqSet_inv_rect_Type0 hterm h1 =
  80   let hcut = deqSet_rect_Type0 h1 hterm in hcut __
  81
  82 (** val beqb : Bool.bool -> Bool.bool -> Bool.bool **)
  83 let beqb b1 b2 =
  84   match b1 with
  85   | Bool.True -> b2
  86   | Bool.False -> Bool.notb b2
  87
  88 (** val deqBool : deqSet **)
  89 let deqBool =
  90   Obj.magic beqb
  91
  92 (** val eq_option :
  93     deqSet -> __ Types.option -> __ Types.option -> Bool.bool **)
  94 let eq_option a a1 a2 =
  95   match a1 with
  96   | Types.None ->
  97     (match a2 with
  98      | Types.None -> Bool.True
  99      | Types.Some x -> Bool.False)
 100   | Types.Some a1' ->
 101     (match a2 with
 102      | Types.None -> Bool.False
 103      | Types.Some a2' -> eqb a a1' a2')
 104
 105 (** val deqOption : deqSet -> deqSet **)
 106 let deqOption a =
 107   Obj.magic (eq_option a)
 108
 109 (** val eq_pairs :
 110     deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod ->
 111     Bool.bool **)
 112 let eq_pairs a b p1 p2 =
 113   Bool.andb (eqb a p1.Types.fst p2.Types.fst)
 114     (eqb b p1.Types.snd p2.Types.snd)
 115
 116 (** val deqProd : deqSet -> deqSet -> deqSet **)
 117 let deqProd a b =
 118   Obj.magic (eq_pairs a b)
 119
 120 (** val eq_sum :
 121     deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool **)
 122 let eq_sum a b p1 p2 =
 123   match p1 with
 124   | Types.Inl a1 ->
 125     (match p2 with
 126      | Types.Inl a2 -> eqb a a1 a2
 127      | Types.Inr b2 -> Bool.False)
 128   | Types.Inr b1 ->
 129     (match p2 with
 130      | Types.Inl a2 -> Bool.False
 131      | Types.Inr b2 -> eqb b b1 b2)
 132
 133 (** val deqSum : deqSet -> deqSet -> deqSet **)
 134 let deqSum a b =
 135   Obj.magic (eq_sum a b)
 136
 137 (** val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool **)
 138 let eq_sigma a p1 p2 =
 139   let a1 = p1 in let a2 = p2 in eqb a a1 a2
 140
 141 (** val deqSig : deqSet -> deqSet **)
 142 let deqSig a =
 143   Obj.magic (eq_sigma a)
 144