extracted/jmeq.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 type sigma =
  12   __
  13   (* singleton inductive, whose constructor was mk_Sigma *)
  14
  15 val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1
  16
  17 val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1
  18
  19 val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1
  20
  21 val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1
  22
  23 val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1
  24
  25 val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1
  26
  27 val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
  28
  29 val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
  30
  31 val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
  32
  33 val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
  34
  35 val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
  36
  37 type p1 = __
  38
  39 val p2 : sigma -> p1
  40
  41 val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2
  42
  43 val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2
  44
  45 val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2
  46
  47 val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2
  48
  49 val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2
  50
  51 val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2
  52
  53 val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
  54
  55 val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
  56
  57 val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
  58
  59 val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
  60
  61 val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
  62
  63 val jmeq_discr : 'a1 -> 'a2 -> __
  64
  65 val cast : 'a1 -> 'a2
  66
  67 type ('a, 'x) curry = 'x
  68
  69 val g : 'a1 -> 'a2 -> 'a1 -> 'a2
  70
  71 type 'p pP = 'p
  72
  73 val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP
  74
  75 val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2
  76