extracted/logic.mli

   1 open Preamble
   2
   3 open Core_notation
   4
   5 open Pts
   6
   7 open Hints_declaration
   8
   9 val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2
  10
  11 val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2
  12
  13 val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2
  14
  15 val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2
  16
  17 val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2
  18
  19 val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2
  20
  21 val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2
  22
  23 val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
  24
  25 val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2
  26
  27 val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2
  28
  29 val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2
  30
  31 val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2
  32
  33 val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2
  34
  35 val eq_coerc : 'a1 -> 'a2
  36
  37 val true_rect_Type4 : 'a1 -> 'a1
  38
  39 val true_rect_Type5 : 'a1 -> 'a1
  40
  41 val true_rect_Type3 : 'a1 -> 'a1
  42
  43 val true_rect_Type2 : 'a1 -> 'a1
  44
  45 val true_rect_Type1 : 'a1 -> 'a1
  46
  47 val true_rect_Type0 : 'a1 -> 'a1
  48
  49 val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1
  50
  51 val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1
  52
  53 val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1
  54
  55 val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1
  56
  57 val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1
  58
  59 val true_discr : __ -> __
  60
  61 val false_rect_Type4 : __ -> 'a1
  62
  63 val false_rect_Type5 : __ -> 'a1
  64
  65 val false_rect_Type3 : __ -> 'a1
  66
  67 val false_rect_Type2 : __ -> 'a1
  68
  69 val false_rect_Type1 : __ -> 'a1
  70
  71 val false_rect_Type0 : __ -> 'a1
  72
  73 val not_rect_Type4 : (__ -> 'a1) -> 'a1
  74
  75 val not_rect_Type5 : (__ -> 'a1) -> 'a1
  76
  77 val not_rect_Type3 : (__ -> 'a1) -> 'a1
  78
  79 val not_rect_Type2 : (__ -> 'a1) -> 'a1
  80
  81 val not_rect_Type1 : (__ -> 'a1) -> 'a1
  82
  83 val not_rect_Type0 : (__ -> 'a1) -> 'a1
  84
  85 val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1
  86
  87 val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1
  88
  89 val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1
  90
  91 val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1
  92
  93 val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1
  94
  95 val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1
  96
  97 val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1
  98
  99 val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1
 100
 101 val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1
 102
 103 val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1
 104
 105 val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1
 106
 107 val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1
 108
 109 val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1
 110
 111 val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1
 112
 113 val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1
 114
 115 val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1
 116
 117 val r0 : 'a1 -> 'a1
 118
 119 val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2
 120
 121 val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3
 122
 123 val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4
 124
 125 val r4 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5
 126
 127 val streicherK : 'a1 -> 'a2 -> 'a2
 128