extracted/deqsets.mli

   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
  24 val deqSet_rect_Type5 :
  25   (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
  26
  27 val deqSet_rect_Type3 :
  28   (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
  29
  30 val deqSet_rect_Type2 :
  31   (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
  32
  33 val deqSet_rect_Type1 :
  34   (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
  35
  36 val deqSet_rect_Type0 :
  37   (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
  38
  39 type carr
  40
  41 val eqb : deqSet -> __ -> __ -> Bool.bool
  42
  43 val deqSet_inv_rect_Type4 :
  44   deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
  45
  46 val deqSet_inv_rect_Type3 :
  47   deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
  48
  49 val deqSet_inv_rect_Type2 :
  50   deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
  51
  52 val deqSet_inv_rect_Type1 :
  53   deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
  54
  55 val deqSet_inv_rect_Type0 :
  56   deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
  57
  58 val beqb : Bool.bool -> Bool.bool -> Bool.bool
  59
  60 val deqBool : deqSet
  61
  62 val eq_option : deqSet -> __ Types.option -> __ Types.option -> Bool.bool
  63
  64 val deqOption : deqSet -> deqSet
  65
  66 val eq_pairs :
  67   deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod -> Bool.bool
  68
  69 val deqProd : deqSet -> deqSet -> deqSet
  70
  71 val eq_sum :
  72   deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool
  73
  74 val deqSum : deqSet -> deqSet -> deqSet
  75
  76 val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool
  77
  78 val deqSig : deqSet -> deqSet
  79