extracted/setoids.mli

   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 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
  19
  20 val setoid_rect_Type5 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
  21
  22 val setoid_rect_Type3 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
  23
  24 val setoid_rect_Type2 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
  25
  26 val setoid_rect_Type1 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
  27
  28 val setoid_rect_Type0 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
  29
  30 type std_supp
  31
  32 val setoid_inv_rect_Type4 :
  33   setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
  34
  35 val setoid_inv_rect_Type3 :
  36   setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
  37
  38 val setoid_inv_rect_Type2 :
  39   setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
  40
  41 val setoid_inv_rect_Type1 :
  42   setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
  43
  44 val setoid_inv_rect_Type0 :
  45   setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
  46
  47 val as_std : setoid
  48
  49 val std_prod : setoid -> setoid -> setoid
  50
  51 val std_union : setoid -> setoid -> setoid
  52